1. 07 Oct, 2019 1 commit
  2. 01 Oct, 2019 1 commit
  3. 19 Sep, 2019 5 commits
    • Robbert's avatar
      Merge branch 'robbert/issue42' into 'master' · 9041e6d8
      Robbert authored
      Disambiguate Haskell-style notations for partially applied operators
      
      Closes #42
      
      See merge request !93
      9041e6d8
    • Robbert Krebbers's avatar
      CHANGELOG entry. · 3a1f5195
      Robbert Krebbers authored
      3a1f5195
    • Robbert Krebbers's avatar
      Disambiguate Haskell-style notations for partially operators. · 45690e49
      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")
      ```
      45690e49
    • Robbert's avatar
      Merge branch 'btt-on-coinductive' into 'master' · b53cbe77
      Robbert authored
      Fix w.r.t. coq/coq#10764.
      
      See merge request !98
      b53cbe77
    • Pierre-Marie Pédrot's avatar
      Fix w.r.t. coq/coq#10764. · ddb36d24
      Pierre-Marie Pédrot authored
      ddb36d24
  4. 12 Sep, 2019 1 commit
  5. 11 Sep, 2019 4 commits
  6. 05 Sep, 2019 1 commit
    • Robbert Krebbers's avatar
      Avoid use of `solve_proper`. · c579b46c
      Robbert Krebbers authored
      Due to Coq bug #10480 or #10474 it actually used `Morphisms.solve_proper`
      instead of the version of std++. The version in std++ can inherently
      not solve this, so I changed it into a manual proof.
      c579b46c
  7. 29 Aug, 2019 3 commits
  8. 27 Aug, 2019 1 commit
  9. 26 Aug, 2019 5 commits
  10. 24 Aug, 2019 3 commits
  11. 23 Aug, 2019 3 commits
  12. 14 Aug, 2019 4 commits
  13. 13 Aug, 2019 3 commits
  14. 07 Aug, 2019 1 commit
  15. 13 Jul, 2019 4 commits