Update to latest Coq 8.15 and mathcomp 1.14 (!184) · Merge requests · RT-PROOFS / PROSA - Formally Proven Schedulability Analysis · GitLab

Snippets Groups Projects

Merged Björn Brandenburg requested to merge coq-version-bump into master 3 years ago

Feb 17, 2022
- Restore compatibility with Coq 8.13 · be40b98b
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 3 years ago
  
  be40b98b
- examples of how to avoid `apply with` · 5a146cd3
  Pierre Roux authored 3 years ago and Björn Brandenburg committed 3 years ago
  
  5a146cd3
Feb 16, 2022
- Rename arguments of [apply _ with (NAME0 := _)] · e078c510
  Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago
  
  From changelog of Coq version 8.15: Changed: [apply with] does not rename arguments unless using compatibility flag Apply With Renaming (#13837, fixes #13759, by Gaëtan Gilbert). So, this commit replaces all occurrences of [apply L with (NAME0 := V)] to [apply L with (NAME := V)]
  e078c510
- update Alectryon image · 1959a478
  Björn Brandenburg authored 3 years ago
  
  1959a478
- coqdoc: remove unnecessary --coqlib flag · db035b16
  Björn Brandenburg authored 3 years ago
  
  The default works just fine (nowadays), so let's use that.
  db035b16
- bump supported Coq and mathcomp versions and update CI · 7984fa01
  Björn Brandenburg authored 3 years ago
  
  7984fa01