- 26 Apr, 2017 1 commit
-
-
Benoit Viguier authored
-
- 01 Apr, 2017 1 commit
-
-
Robbert Krebbers authored
This is needed to use coq-stdpp in developments with -type-in-type as set_unfold will otherwise unify with any hyp, causing the set_solver tactic to break.
-
- 28 Mar, 2017 2 commits
-
-
Benoit Viguier authored
-
Benoit Viguier authored
-
- 20 Mar, 2017 1 commit
-
-
Robbert Krebbers authored
This way, we get more definitional equalities.
-
- 17 Mar, 2017 4 commits
-
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- 15 Mar, 2017 9 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- 14 Mar, 2017 1 commit
-
-
Ralf Jung authored
-
- 11 Mar, 2017 1 commit
-
-
Robbert Krebbers authored
-
- 09 Mar, 2017 4 commits
-
-
Robbert Krebbers authored
To be consistent with Iris, see Iris commit 9ee62b3a.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 08 Mar, 2017 1 commit
-
-
Robbert Krebbers authored
-
- 01 Mar, 2017 1 commit
-
-
Ralf Jung authored
-
- 23 Feb, 2017 1 commit
-
- 22 Feb, 2017 4 commits
-
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Ralf Jung authored
It is sometimes not desirable to do so.
-
Robbert Krebbers authored
-
- 19 Feb, 2017 1 commit
-
-
Robbert Krebbers authored
For example, instead of: Notation "( X ⊆ )" We now use: Notation "( X ⊆)" We were already doing this for = and ≡. This solves some conflicts with the notations of MetaCoq.
-
- 17 Feb, 2017 1 commit
-
-
Benoit Viguier authored
-
- 16 Feb, 2017 3 commits
-
-
Ralf Jung authored
-
Robbert Krebbers authored
To make it consistent with Forall_impl and map_Forall_impl. Also, put the premises in the same order as those lemmas.
-
Robbert Krebbers authored
-
- 15 Feb, 2017 2 commits
-
-
Robbert Krebbers authored
-
Benoit Viguier authored
also add html folder to .gitignore so generated doc is not added to the repo
-
- 14 Feb, 2017 2 commits