- Jan 13, 2020
- Dec 19, 2019
-
-
Ralf Jung authored
-
- Dec 06, 2019
-
-
Ralf Jung authored
-
- Nov 22, 2019
- Nov 21, 2019
-
-
Robbert Krebbers authored
Opaquify proofs in gmap_partial_alter (fix #46) Closes #46 See merge request !106
-
- Ensure gmap well-formedness proofs are fully opaque. - Use pattern-matching lambdas over lets.
-
- Nov 11, 2019
-
-
Robbert Krebbers authored
Add lemmas regarding set_seq See merge request !105
-
Simon Friis Vindum authored
-
- Nov 07, 2019
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
Remove `:>>` subclass instance declarations See merge request !104
-
Robbert Krebbers authored
There are not documented in https://coq.inria.fr/refman/addendum/type-classes.html?highlight=class#coq:cmd.class, and they don't have any advantage, so it's better to stop using them.
-
- Nov 06, 2019
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Nov 02, 2019
-
-
Ralf Jung authored
-
- Nov 01, 2019
-
-
Tej Chajed authored
See https://github.com/coq/coq/pull/10947 (.coqdeps.d now uses the name of the Coq Makefile) and https://github.com/coq/coq/pull/8642 (Coq now generates empty interface files *.vos when compiling).
-
Robbert Krebbers authored
Add congruence lemmas for closures See merge request !102
-
Amin Timany authored
-
Robbert Krebbers authored
Add two useful lemmas See merge request !101
-
Amin Timany authored
-
- Oct 31, 2019
-
-
Ralf Jung authored
-
Ralf Jung authored
Mentioned Windows line ending fix in README See merge request iris/stdpp!100
-
Ralf Jung authored
-
William Mansky authored
-
- Oct 07, 2019
-
-
Robbert Krebbers authored
Generalize `list_find` lemmas to become bi-implications. See merge request !99
-
- Oct 01, 2019
-
-
Robbert Krebbers authored
Thanks to @jules for the suggestion and an initial proof.
-
- Sep 19, 2019
-
-
Robbert Krebbers authored
Disambiguate Haskell-style notations for partially applied operators Closes #42 See merge request !93
-
Robbert Krebbers authored
-
Robbert Krebbers authored
For example, change `(!! i)` into `(.!! x)` so that `!!` can also be used as a prefix, as done in VST for example. This closes issue #42. I have used the `sed` script below. This script took care of nearly all uses apart from a few occurrences where a space was missing, e.g. `(,foo)`. In this case, `coqc` will just fail, allowing one to patch up things manually. The script is slightly too eager on Iris developments, where it also replaces `($ ...)` introduction patterns. When porting Iris developments you thus may want to remove the line for `$`. ``` sed ' s/(= /(.= /g; s/ =)/ =.)/g; s/(≠ /(.≠ /g; s/ ≠)/ ≠.)/g; s/(≡ /(.≡ /g; s/ ≡)/ ≡.)/g; s/(≢ /(.≢ /g; s/ ≢)/ ≢.)/g; s/(∧ /(.∧ /g; s/ ∧)/ ∧.)/g; s/(∨ /(.∨ /g; s/ ∨)/ ∨.)/g; s/(
/(. /g; s/ )/ .)/g; s/(→ /(.→ /g; s/ →)/ →.)/g; s/($ /(.$ /g; s/(∘ /(.∘ /g; s/ ∘)/ ∘.)/g; s/(, /(., /g; s/ ,)/ ,.)/g; s/(∘ /(.∘ /g; s/ ∘)/ ∘.)/g; s/(∪ /(.∪ /g; s/ ∪)/ ∪.)/g; s/(⊎ /(.⊎ /g; s/ ⊎)/ ⊎.)/g; s/(∩ /(.∩ /g; s/ ∩)/ ∩.)/g; s/(∖ /(.∖ /g; s/ ∖)/ ∖.)/g; s/(⊆ /(.⊆ /g; s/ ⊆)/ ⊆.)/g; s/(⊈ /(.⊈ /g; s/ ⊈)/ ⊈.)/g; s/(⊂ /(.⊂ /g; s/ ⊂)/ ⊂.)/g; s/(⊄ /(.⊄ /g; s/ ⊄)/ ⊄.)/g; s/(∈ /(.∈ /g; s/ ∈)/ ∈.)/g; s/(∉ /(.∉ /g; s/ ∉)/ ∉.)/g; s/(≫= /(.≫= /g; s/ ≫=)/ ≫=.)/g; s/(!! /(.!! /g; s/ !!)/ !!.)/g; s/(⊑ /(.⊑ /g; s/ ⊑)/ ⊑.)/g; s/(⊓ /(.⊓ /g; s/ ⊓)/ ⊓.)/g; s/(⊔ /(.⊔ /g; s/ ⊔)/ ⊔.)/g; s/(:: /(.:: /g; s/ ::)/ ::.)/g; s/(++ /(.++ /g; s/ ++)/ ++.)/g; s/(≡ₚ /(.≡ₚ /g; s/ ≡ₚ)/ ≡ₚ.)/g; s/(≢ₚ /(.≢ₚ /g; s/ ≢ₚ)/ ≢ₚ.)/g; s/(::: /(.::: /g; s/ :::)/ :::.)/g; s/(+++ /(.+++ /g; s/ +++)/ +++.)/g; ' -i $(find -name "*.v") ```
-