 14 Jan, 2018 1 commit


Robbert Krebbers authored
This is needed so that it can be used be used as a combinator for defining induction schemes for mutually inductive types.

 12 Nov, 2017 1 commit


Robbert Krebbers authored
This follows the associativity in Haskell. So, something like f <$> g <$> h Is now parsed as: (f <$> g) <$> h Since the functor is a generalized form of function application, this also now also corresponds with the associativity of function application, which is also left associative.

 09 Nov, 2017 1 commit


Robbert Krebbers authored

 28 Oct, 2017 1 commit


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

 24 Sep, 2017 1 commit


Robbert Krebbers authored

 21 Sep, 2017 1 commit


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

 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 1 commit


Robbert Krebbers authored

 25 May, 2017 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 20 Mar, 2017 1 commit


Robbert Krebbers authored
This way, we get more definitional equalities.

 17 Mar, 2017 1 commit


Ralf Jung authored

 15 Mar, 2017 1 commit


Robbert Krebbers authored

 01 Mar, 2017 1 commit


Ralf Jung authored

 09 Feb, 2017 1 commit


Robbert Krebbers authored

 31 Jan, 2017 10 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
Rename:  prefix_of > prefix and suffix_of > suffix because that saves keystrokes in lemma names. However, keep the infix notations with l1 `prefix_of` l2 and l1 `suffix_of` l2 because those are easier to read.  change the notation l1 `sublist` l2 into l1 `sublist_of` l2 to be consistent.  rename contains > submseteq and use the notation ⊆+

Robbert Krebbers authored

Ralf Jung authored

Robbert Krebbers 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

Robbert Krebbers authored

Robbert Krebbers authored
Also make names more consistent.

Ralf Jung authored

 09 Dec, 2016 1 commit


Ralf Jung authored

 06 Dec, 2016 1 commit


Robbert Krebbers authored

 23 Nov, 2016 1 commit


Robbert Krebbers authored

 13 Oct, 2016 1 commit


Ralf Jung authored

 20 Sep, 2016 2 commits


Robbert Krebbers authored
This also solves a name clash with the extension order of CMRAs.

Robbert Krebbers authored

 24 Aug, 2016 1 commit


Robbert Krebbers authored

 08 Aug, 2016 1 commit


Ralf Jung authored
With Coq 8.6, you can no longer have intro patterns that give more names than the constructor has. Also, patterns with too few names are now interpreted as filling up with "?", rather than putting the unnamed parts into the goal again. Furthermore, it seems the behavior of "simplify_eq/=" changed, I guess hypotheses are considered in different order now. I managed to work around this, but it all seem kind of fragile. The next compilation failure is an "Anyomaly: ... Please report", so that's what I will do.

 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.

 30 Jun, 2016 1 commit


JacquesHenri Jourdan authored

 27 May, 2016 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 22 May, 2016 1 commit


Robbert Krebbers authored
Initial commit by Amin Timany.
