create_makefile.sh · 11fb68b6d120d923be7bb5df604add63276667c7 · Lasse Blaauwbroek / PROSA - Formally Proven Schedulability Analysis

Forked from RT-PROOFS / PROSA - Formally Proven Schedulability Analysis

Source project has a limited visibility.

7 years ago

Make Prosa compatible with Coq 8.7.0 and Mathcomp 1.6.4 · b6c93d38

- Remove Require declarations from Modules.
- Small fixes due to changes in the type checker.
- Generate _CoqProject with Makefile and remove spurious warnings from ssreflect.

b6c93d38

History

Make Prosa compatible with Coq 8.7.0 and Mathcomp 1.6.4

Felipe Cerqueira authored 7 years ago

- Remove Require declarations from Modules.
- Small fixes due to changes in the type checker.
- Generate _CoqProject with Makefile and remove spurious warnings from ssreflect.