- Nov 22, 2024
-
-
Pierre Courtieu authored
coq 8.20 has a small regression with lia. + some small stdlib changes.
-
- Oct 08, 2024
-
-
Pierre Courtieu authored
-
- Oct 07, 2024
-
-
Pierre Courtieu authored
-
Pierre Courtieu authored
-
- Jul 23, 2024
-
-
Lionel Rieg authored
-
- Jul 16, 2024
-
-
Lionel Rieg authored
-
- Jun 18, 2024
-
-
Lionel Rieg authored
-
- Jun 11, 2024
-
-
Lionel Rieg authored
-
- Mar 13, 2023
-
-
Sébastien Bouchard authored
-
- Feb 14, 2023
-
-
Sébastien Bouchard authored
-
- Sep 12, 2022
-
-
Sébastien Bouchard authored
-
- Jul 12, 2022
-
-
Lionel Rieg authored
-
- Feb 18, 2022
-
-
Sébastien Bouchard authored
-
Pierre Courtieu authored
-
- Feb 15, 2022
-
-
Lionel Rieg authored
-
- Dec 17, 2021
-
-
Pierre Courtieu authored
-
- May 11, 2021
-
-
Lionel Rieg authored
-
- Mar 24, 2021
-
-
Pierre Courtieu authored
Dropped <=v8.11 because: 1) #[export] not supported but needed 2) Some definitions we use (e.g. Bool.le) do not exist in before v8.12. Both problems are fixable but it is probably not worth the effort.
-
- Oct 03, 2020
-
-
Pierre Courtieu authored
-
- Oct 02, 2020
-
-
Pierre Courtieu authored
-
- Apr 28, 2020
-
-
Pierre Courtieu authored
-
- Apr 20, 2020
-
-
Pierre Courtieu authored
-
Pierre Courtieu authored
First try in this normalization process. Several cleaning ideas: 1) Avoid side effects on instances as much as possible. The general goal is that the presence/absence and the order of "Require Import" should not break a development too easily. 2) Have systematic header (that we can generate automatically) for each "model setting" wrt synchronicity, topology, felxibility, observation, etc. Strategy: - avoiding Require Export. - avoiding Import as much as possible. Only very generic definitions are allowed to be imported (Require is of course allowed). Reason: it also imports Non Local Instances and notations. We may swithc to Local Instance and Local Notation instead, and allow more imports later. - avoid Global Instances as much as possible.
-
- Apr 17, 2020
-
-
Pierre Courtieu authored
Thanks to Proofgeneral which insert them automatically.
-
- Nov 14, 2019
-
-
Lionel Rieg authored
-
Lionel Rieg authored
-
Lionel Rieg authored
-
Lionel Rieg authored
-
- Sep 29, 2019
-
-
Lionel Rieg authored
-
- Apr 03, 2019
-
-
Lionel Rieg authored
The axioms are exculded middle and Eq_dep.eq_rect_eq.
-
- Mar 12, 2019
-
-
Lionel Rieg authored
-
Lionel Rieg authored
-
- Mar 11, 2019
-
-
Lionel Rieg authored
-
Lionel Rieg authored
-
- Jan 25, 2019
-
-
Lionel Rieg authored
-
- Nov 23, 2018
-
-
Lionel Rieg authored
-
- Sep 15, 2018
-
-
Lionel Rieg authored
-
Lionel Rieg authored
-
- Sep 01, 2018
-
-
Lionel Rieg authored
-
- Aug 09, 2018
-
-
Lionel Rieg authored
Also requires removing lift_compose as it does not hold for this spectrum
-