- 19 Jul, 2020 6 commits
-
-
Tej Chajed authored
-
Tej Chajed authored
Re-implement passing identifier back to Ltac1 See merge request !5
-
Tej Chajed authored
Add tests and test infrastructure See merge request !4
-
Tej Chajed authored
This implementation avoids use of Unsafe, so it is compatible with v8.11 and forward, and also has the benefit of being simpler.
-
Tej Chajed authored
-
Tej Chajed authored
-
- 15 Jul, 2020 1 commit
-
-
Ralf Jung authored
-
- 25 May, 2020 1 commit
-
-
Ralf Jung authored
-
- 29 Apr, 2020 4 commits
-
-
Tej Chajed authored
Correct usage instructions: replace `Require` with `Require Import` See merge request !3
-
Paolo G. Giarrusso authored
-
Paolo G. Giarrusso authored
-
Paolo G. Giarrusso authored
The fact that `Require` seems to work is a misfeature (https://github.com/coq/coq/issues/12206). Worse, unlike you'd expect from `Require`, indirect `Require` doesn't work.
-
- 07 Apr, 2020 2 commits
-
-
Paolo G. Giarrusso authored
- 06 Apr, 2020 2 commits
-
-
Tej Chajed authored
-
Tej Chajed authored
-
- 30 Mar, 2020 1 commit
-
-
Tej Chajed authored
-
- 27 Mar, 2020 8 commits
-
-
Tej Chajed authored
-
Ralf Jung authored
-
Tej Chajed authored
make LICENSE consistent with Iris See merge request !1
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
- 25 Mar, 2020 3 commits
-
-
Tej Chajed authored
-
Tej Chajed authored
-
Tej Chajed authored
-
- 24 Mar, 2020 4 commits
-
-
Tej Chajed authored
-
Tej Chajed authored
-
Tej Chajed authored
-
Tej Chajed authored
-