Support mathcomp 1.11.0 and Coq 8.12 (!104) · Merge requests · RT-PROOFS / PROSA - Formally Proven Schedulability Analysis

Merged Björn Brandenburg requested to merge coq-8.12 into master 4 years ago

Aug 06, 2020

still allow compilation with mathcomp 1.10.0 & Coq 8.11 · 30d8f275

Before mathcomp 1.11.0 (which requires Coq 8.12), case analysis
doesn't automatically rewrite destructed `minn` premises, so "try"
this manually until we drop support for mathcomp 1.11.0.

30d8f275

Aug 05, 2020
- still allow compilation with mathcomp 1.10.0 · f93c9a09
  Björn Brandenburg authored 4 years ago
  
  Can't rely on arg_maxnP just yet.
  f93c9a09
- fix deprecation warning in classic global schedule · bd0e5427
  Björn Brandenburg authored 4 years ago
  
  This change breaks compatibility with mathcomp < 1.10.
  bd0e5427
- fix name clash in classic · 5312542f
  Björn Brandenburg authored 4 years ago
  
  There's now also a `findP` in ssreflect's seq library.
  5312542f
- Fixed error in classic · 224fa258
  Marco Maida authored 4 years ago
  
  224fa258
- Replaced `omega` with `lia` · 66fe0910
  Marco Maida authored 4 years ago
  
  66fe0910
- Fixed compilation errors (without classic) · 3eb23cbe
  Marco Maida authored 4 years ago
  
  3eb23cbe
Aug 04, 2020
- update opam spec file · 5b509b25
  Björn Brandenburg authored 4 years ago
  
  5b509b25
- CI: remove older versions no longer supported · 131f1998
  Björn Brandenburg authored 4 years ago
  
  131f1998
- CI: add new jobs for mathcomp 1.11 and Coq 8.12 · e48ad1ec
  Björn Brandenburg authored 4 years ago
  
  e48ad1ec
- CI: don't hardcode version multiple times · 7cd0103c
  Björn Brandenburg authored 4 years ago
  
  7cd0103c

Support mathcomp 1.11.0 and Coq 8.12

Merge request reports

Activity