- Nov 16, 2021
-
-
Robbert Krebbers authored
-
- Nov 08, 2021
- Nov 06, 2021
-
-
Ralf Jung authored -
Lennard Gäher authored
-
- Nov 05, 2021
-
-
Ralf Jung authored
-
-
- Oct 26, 2021
-
-
Paolo G. Giarrusso authored
-
- Oct 01, 2021
-
-
Armaël Guéneau authored
-
- Sep 06, 2021
-
-
Ralf Jung authored
-
Armaël Guéneau authored
With large proof contexts and lemmas with many forall quantifiers, iIntoEmpValid can become quite slow. This makes it go faster by adding "fast paths" for the -> and forall cases, gated by Ltac pattern matching (which is faster than trying to unify with refine and fail).
-
- Sep 05, 2021
-
-
Ralf Jung authored
-
- Sep 01, 2021
-
-
Ralf Jung authored
-
- Jul 30, 2021
-
-
Simon Friis Vindum authored -
Simon Friis Vindum authored
-
- Jul 28, 2021
- Jul 26, 2021
-
-
Ralf Jung authored
-
-
Hai Dang authored
-
Ralf Jung authored
-
Michael Sammler authored
-
- Jul 25, 2021
-
-
-
Paolo G. Giarrusso authored
-
- Jul 23, 2021
-
-
Paolo G. Giarrusso authored
-
-
- Jul 22, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jul 19, 2021
-
-
Ralf Jung authored
-
- Jul 18, 2021
-
-
Ralf Jung authored
-
Paolo G. Giarrusso authored
In 13c5c1ad I strengthened bi.persistent_sep_dup to support propositions that are persistent and either affine or absorbing; do the same for `persistent_fractional`.
-
- Jul 16, 2021
-
-
Robbert Krebbers authored
-
- Jun 20, 2021
-
-
Ralf Jung authored
-
- Jun 19, 2021
-
-
Paolo G. Giarrusso authored
Include workaround for Coq bug #14441, and drop now-failing test for that Coq bug.
-
- Jun 18, 2021
- Jun 17, 2021
-
-
Ralf Jung authored
-
Paolo G. Giarrusso authored
-
