 28 Oct, 2017 4 commits


Ralf Jung authored

Robbert Krebbers authored
This addresses some concerns in !5.

Robbert Krebbers authored
This way, we will be compabile with Iris's heap_lang, which puts ;; at level 100.

Ralf Jung authored

 13 Oct, 2017 1 commit


Ralf Jung authored

 10 Oct, 2017 1 commit


Ralf Jung authored

 06 Oct, 2017 1 commit


Robbert Krebbers authored

 21 Sep, 2017 2 commits


Robbert Krebbers authored

Robbert Krebbers authored
This allows for more control over `Hint Mode`.

 18 Sep, 2017 1 commit


Robbert Krebbers authored

 17 Sep, 2017 1 commit


Robbert Krebbers authored
This provides significant robustness against looping type class search. As a consequence, at many places throughout the library we had to add additional typing information to lemmas. This was to be expected, since most of the old lemmas were ambiguous. For example: Section fin_collection. Context `{FinCollection A C}. size_singleton (x : A) : size {[ x ]} = 1. In this case, the lemma does not tell us which `FinCollection` with elements `A` we are talking about. So, `{[ x ]}` could not only refer to the singleton operation of the `FinCollection A C` in the section, but also to any other `FinCollection` in the development. To make this lemma unambigious, it should be written as: Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1. In similar spirit, lemmas like the one below were also ambiguous: Lemma lookup_alter_None {A} (f : A → A) m i j : alter f i m !! j = None
↔ m !! j = None. It is not clear which finite map implementation we are talking about. To make this lemma unambigious, it should be written as: Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j : alter f i m !! j = None↔ m !! j = None. That is, we have to specify the type of `m`.

 08 Sep, 2017 1 commit


Robbert Krebbers authored
See also Coq bug #5712.

 02 Sep, 2017 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
Before, we often had to insert awkward casts when using them. Also, the generality of also having them on Type, is probably not useful.

Robbert Krebbers authored

 17 Aug, 2017 1 commit


Robbert Krebbers authored

 08 Aug, 2017 1 commit


Robbert Krebbers authored

 17 Mar, 2017 3 commits


Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored

 15 Mar, 2017 1 commit


Robbert Krebbers authored

 09 Mar, 2017 1 commit


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.

 10 Feb, 2017 1 commit


Robbert Krebbers authored
Some were already maximally implicit, some were not. Now it is consistent.

 31 Jan, 2017 5 commits


Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored
This approach is originally by Robbert

Ralf Jung authored

Ralf Jung authored
This patch was created using find name *.v  xargs L 1 awk i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 ' and some minor manual editing

 22 Nov, 2016 1 commit


Robbert Krebbers authored
We do this by introducing a type class UpClose with notation ↑. The reason for this change is as follows: since `nclose : namespace → coPset` is declared as a coercion, the notation `nclose N ⊆ E` was pretty printed as `N ⊆ E`. However, `N ⊆ E` could not be typechecked because type checking goes from left to right, and as such would look for an instance `SubsetEq namespace`, which causes the right hand side to be illtyped.

 15 Nov, 2016 1 commit


Ralf Jung authored

 10 Nov, 2016 1 commit


Robbert Krebbers authored
Having Is_true as a type class caused problems with rewrite: when the rewrited lemma has a premise of the shape Is_true, the rewrite tactic will complain that it cannot find a type class instance, instead of generating a goal for that premise.

 20 Sep, 2016 1 commit


Robbert Krebbers authored

 14 Sep, 2016 1 commit


JacquesHenri Jourdan authored
This makes the typeclass mechanism able to use instances like [Is_true X > Blah], where X reduces to X.

 19 Aug, 2016 1 commit


Robbert Krebbers authored
There is still the reals stuff, which is caused by importint Psatz (needed for lia) and eq_rect_eq which is caused by importint Eqdep_dec.

 08 Aug, 2016 1 commit


JacquesHenri Jourdan authored

 27 Jul, 2016 2 commits


Robbert Krebbers authored
This reverts commit 20b4ae55bdf00edb751ccdab3eb876cb9b13c99f, which does not seem to work with Coq 8.5pl2 (I accidentally tested with 8.5pl1).

Robbert Krebbers authored
This makes type checking more directed, and somewhat more predictable. On the downside, it makes it impossible to declare the singleton on lists as an instance of SingletonM and the insert and alter operations on functions as instances of Alter and Insert. However, these were not used often anyway.

 22 Jul, 2016 1 commit


Robbert Krebbers authored
There was not really a need for the lattice type classes, so I removed these.
