 29 Jan, 2019 40 commits


Robbert Krebbers authored

 23 Jan, 2019 40 commits


Maxime Dénès authored
This is in preparation for coq/coq#9274.

 28 Nov, 2018 40 commits


Tej Chajed authored
Adding a hint without a database now triggers a deprecation warning in Coq master (https://github.com/coq/coq/pull/8987).

 29 May, 2018 40 commits


Ralf Jung authored

 28 May, 2018 40 commits


Ralf Jung authored

 24 May, 2018 40 commits


Ralf Jung authored
The notation was parsingonly and all it did was reorder the arguments for from_option. This creates just a needless divergence between what is written and what is printed. Also, removing it frees the name for maybe introducing a function or notation `default` with a type like `T > option T > T`.

 05 Apr, 2018 40 commits


Robbert Krebbers authored
This followed from discussions in https://gitlab.mpisws.org/FP/iriscoq/merge_requests/134

 31 Jan, 2018 40 commits


Robbert Krebbers authored

 12 Nov, 2017 40 commits


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.

 28 Oct, 2017 40 commits


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

Ralf Jung authored

 17 Sep, 2017 40 commits


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 40 commits


Robbert Krebbers authored
See also Coq bug #5712.

 15 Mar, 2017 40 commits


Robbert Krebbers authored

 09 Feb, 2017 40 commits


Robbert Krebbers authored

 31 Jan, 2017 40 commits


Robbert Krebbers authored

Ralf Jung authored

Robbert Krebbers authored

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

 09 Dec, 2016 40 commits


Robbert Krebbers authored
We typically use the _1 and _2 suffix to denote individual directions of a lemmas that is a biimplication.

Ralf Jung authored

 22 Nov, 2016 40 commits


Ralf Jung authored

 16 Nov, 2016 40 commits


Robbert Krebbers authored

 03 Oct, 2016 40 commits


Robbert Krebbers authored

 20 Sep, 2016 40 commits


Robbert Krebbers authored

Robbert Krebbers authored

 27 Jul, 2016 40 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.

 14 Jun, 2016 40 commits


Robbert Krebbers authored

 27 May, 2016 40 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 21 Mar, 2016 40 commits


Robbert Krebbers authored

 03 Mar, 2016 40 commits


Robbert Krebbers authored

 20 Feb, 2016 40 commits


Ralf Jung authored

 17 Feb, 2016 40 commits


Robbert Krebbers authored
simplify_equality => simplify_eq simplify_equality' => simplify_eq/= simplify_map_equality => simplify_map_eq simplify_map_equality' => simplify_map_eq/= simplify_option_equality => simplify_option_eq simplify_list_equality => simplify_list_eq f_equal' => f_equal/= The /= suffixes (meaning: do simpl) are inspired by ssreflect.

Robbert Krebbers authored

 13 Feb, 2016 40 commits


Robbert Krebbers authored
Also, make our redefinition of done more robust under different orders of Importing modules.
