- Sep 29, 2020
-
-
Robbert Krebbers authored
-
- Sep 10, 2020
-
-
Ralf Jung authored
-
- May 28, 2020
-
-
Paolo G. Giarrusso authored
-
- May 24, 2020
-
-
Robbert Krebbers authored
-
- May 23, 2020
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Mar 18, 2020
-
-
Ralf Jung authored
-
- Jan 16, 2020
-
-
Michael Sammler authored
-
- Aug 22, 2019
-
-
Robbert Krebbers authored
-
- Aug 08, 2019
-
-
Paolo G. Giarrusso authored
- And use prop_ext instead of prop_ext_2 in other proofs.
-
- Aug 07, 2019
-
-
Paolo G. Giarrusso authored
-
- Apr 25, 2019
-
-
- Jan 24, 2019
-
-
Maxime Dénès authored
This is in preparation for coq/coq#9274.
-
- Nov 29, 2018
-
-
Tej Chajed authored
Adding a hint without a database now triggers a deprecation warning in Coq master (https://github.com/coq/coq/pull/8987).
-
- Oct 27, 2018
-
-
Robbert Krebbers authored
-
- Jun 11, 2018
-
-
Ralf Jung authored
-
- Jun 10, 2018
-
-
Ralf Jung authored
-
- Jun 05, 2018
-
-
Ralf Jung authored
The BI interface is then instantiated using these laws. In particular, this shows that the rules we claim to be admissible actually are.
-
- Apr 05, 2018
- Mar 22, 2018
-
-
- Mar 21, 2018
-
-
Ralf Jung authored
-
- Mar 19, 2018
-
-
Ralf Jung authored
-
- Mar 07, 2018
- Mar 04, 2018
-
-
Robbert Krebbers authored
-
- Mar 03, 2018
-
-
Jacques-Henri Jourdan authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Based on an earlier MR by @jung.
-
