- 07 May, 2019 40 commits
-
-
charguer authored
-
- 05 Feb, 2019 40 commits
-
-
Armaël Guéneau authored
-
- 07 Jan, 2019 40 commits
-
-
charguer authored
-
- 28 Nov, 2018 40 commits
-
-
Armaël Guéneau authored
-
- 14 Nov, 2018 40 commits
-
-
charguer authored
-
- 13 Nov, 2018 40 commits
-
-
charguer authored
-
- 09 Jul, 2018 40 commits
-
-
Armaël Guéneau authored
-
- 27 Jun, 2018 40 commits
-
-
Armaël Guéneau authored
count has been added to TLC
-
- 22 Jun, 2018 40 commits
-
-
Armaël Guéneau authored
-
- 21 Jun, 2018 40 commits
-
-
Armaël Guéneau authored
-
Armaël Guéneau authored
-
Armaël Guéneau authored
-
Armaël Guéneau authored
-
charguer authored
-
charguer authored
-
charguer authored
-
Armaël Guéneau authored
-
- 20 Jun, 2018 40 commits
-
-
Armaël Guéneau authored
-
- 19 Jun, 2018 40 commits
- 18 Jun, 2018 40 commits
- 11 Jun, 2018 40 commits
-
-
Armaël Guéneau authored
Fix xspec for record operations in presence of several records See merge request !5
-
Armaël Guéneau authored
-
Black Rook authored
-
- 04 Jun, 2018 40 commits
-
-
charguer authored
-
- 28 May, 2018 40 commits
-
-
POTTIER Francois authored
-
- 24 May, 2018 40 commits
-
-
Armaël Guéneau authored
-
Armaël Guéneau authored
-
Armaël Guéneau authored
-
Armaël Guéneau authored
Make CFML work with coq 8.6.1 and newer See merge request !4
-
Armaël Guéneau authored
-
Armaël Guéneau authored
-
Armaël Guéneau authored
It seems the hsimpl tactic was in some cases working thanks to a bug in Ltac pattern matching, introduced in Coq 8.4, and that was fixed in Coq 8.6.1 (https://github.com/coq/coq/issues/5487). The fix implemented here makes hsimpl slightly more powerful in some cases, so proofs may need to be updated.
-
- 23 May, 2018 40 commits
-
-
POTTIER Francois authored
-
POTTIER Francois authored
-
POTTIER Francois authored
-
POTTIER Francois authored
-
POTTIER Francois authored
-
POTTIER Francois authored
-
