-
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") ```Robbert Krebbers authoredFor 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") ```