 29 Jan, 2019 1 commit


Robbert Krebbers authored

 24 Jan, 2019 1 commit


Ralf Jung authored

 19 Jan, 2019 1 commit


Ralf Jung authored

 28 Nov, 2018 1 commit


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

 09 Nov, 2018 1 commit


Robbert Krebbers authored

 04 Nov, 2018 1 commit


Robbert Krebbers authored

 10 Jun, 2018 1 commit


Robbert Krebbers authored

 23 May, 2018 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 27 Apr, 2018 1 commit


Robbert Krebbers authored

 05 Apr, 2018 2 commits


Robbert Krebbers authored
Terminology taken from "A Fresh Look at Separation Algebras and Share" by Dockins et al.

Robbert Krebbers authored

 08 Mar, 2018 1 commit


Robbert Krebbers authored

 21 Nov, 2017 1 commit


Robbert Krebbers authored
This gets rid of the old hack to have specific notations for pairs up to a fixed arity, and moreover allows to do fancy things like: ``` Record test := Test { t1 : nat; t2 : nat }. Definition foo (x : option test) : option nat := ''(Test a1 a2) ← x; Some a1. ```

 31 Oct, 2017 1 commit


Johannes Kloos authored

 21 Sep, 2017 1 commit


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

 08 Sep, 2017 1 commit


Robbert Krebbers authored
See also Coq bug #5712.

 15 Mar, 2017 1 commit


Robbert Krebbers authored

 11 Mar, 2017 1 commit


Robbert Krebbers authored

 09 Mar, 2017 1 commit


Robbert Krebbers authored

 22 Feb, 2017 1 commit


Robbert Krebbers authored

 31 Jan, 2017 3 commits


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

 16 Nov, 2016 1 commit


Robbert Krebbers authored

 07 Nov, 2016 1 commit


JacquesHenri Jourdan authored

 04 Oct, 2016 2 commits


Zhen Zhang authored

Zhen Zhang authored

 20 Sep, 2016 1 commit


Robbert Krebbers authored

 09 Sep, 2016 2 commits


Robbert Krebbers authored

JacquesHenri Jourdan authored

 22 Aug, 2016 1 commit


Robbert Krebbers authored
The previous commit is not really necesarry anymore, but my proof for UIP of types with decidable equality is a bit more general, so I won't revert it.

 04 Aug, 2016 2 commits


Robbert Krebbers authored
Also cleanup the file a bit.

Robbert Krebbers authored

 03 Jul, 2016 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 26 Feb, 2016 1 commit


Robbert Krebbers authored

 20 Feb, 2016 1 commit


Ralf Jung authored

 17 Feb, 2016 2 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
