- 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
-
- Jun 29, 2023
-
-
Sébastien Bouchard authored
-
- Mar 13, 2023
-
-
Sébastien Bouchard authored
-
- Mar 03, 2023
-
-
Sébastien Bouchard authored
-
- Feb 14, 2023
-
-
Sébastien Bouchard authored
-
- Mar 15, 2022
-
-
Sébastien Bouchard authored
-
- May 11, 2021
-
-
Lionel Rieg authored
-
- Jan 25, 2021
-
-
Lionel Rieg authored
-
- Oct 03, 2020
-
-
Pierre Courtieu authored
-
- Oct 02, 2020
-
-
Pierre Courtieu authored
-
- Apr 28, 2020
-
-
Pierre Courtieu authored
-
Pierre Courtieu authored
-
- 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
-
- Sep 29, 2019
-
-
Lionel Rieg authored
-
- Jun 13, 2019
-
-
Lionel Rieg authored
-
- Jun 12, 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
-
- Jan 25, 2019
-
-
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
-
- Jun 25, 2018
-
-
Lionel Rieg authored
Indeed, I don't know how to define it in the general case (lack of rotation). This also means that the generic impossibility proof now depends on its existence.
-
- Jun 16, 2018
-
-
Lionel Rieg authored
-
- Jun 15, 2018
-
-
Lionel Rieg authored
-
Lionel Rieg authored
-
- Nov 30, 2017
-
-
Lionel Rieg authored
-
Lionel Rieg authored
-
- Nov 27, 2017
-
-
Lionel Rieg authored
-
- Oct 27, 2017
-
-
Lionel Rieg authored
-
- Oct 24, 2017
-
-
Lionel Rieg authored
-
- Jul 11, 2017
-
-
Lionel Rieg authored
-