1. 19 Sep, 2019 2 commits
    • 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
    • Pierre-Marie Pédrot's avatar
      Fix w.r.t. coq/coq#10764. · ddb36d24
      Pierre-Marie Pédrot authored
      ddb36d24
  2. 11 Sep, 2019 3 commits
  3. 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
  4. 29 Aug, 2019 1 commit
  5. 26 Aug, 2019 3 commits
  6. 24 Aug, 2019 1 commit
  7. 23 Aug, 2019 2 commits
  8. 14 Aug, 2019 2 commits
  9. 13 Aug, 2019 1 commit
  10. 13 Jul, 2019 3 commits
  11. 09 Jul, 2019 1 commit
  12. 08 Jul, 2019 1 commit
  13. 07 Jul, 2019 4 commits
  14. 05 Jul, 2019 1 commit
  15. 03 Jul, 2019 2 commits
  16. 30 Jun, 2019 2 commits
  17. 28 Jun, 2019 2 commits
  18. 27 Jun, 2019 2 commits
  19. 26 Jun, 2019 3 commits
  20. 25 Jun, 2019 1 commit
  21. 21 Jun, 2019 2 commits