diff options
author | 2002-07-18 20:27:05 +0000 | |
---|---|---|
committer | 2002-07-18 20:27:05 +0000 | |
commit | c52e83c8428bcd4d49ff395c44485217944c5655 (patch) | |
tree | 435f4ba91a8e9d0ceca0e7780c50ef74d31254a1 /etc/coq/queryreplace.v | |
parent | 689027e8088128c4b4fd887479ffcaecba507a88 (diff) |
New files.
Diffstat (limited to 'etc/coq/queryreplace.v')
-rw-r--r-- | etc/coq/queryreplace.v | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/etc/coq/queryreplace.v b/etc/coq/queryreplace.v new file mode 100644 index 00000000..977846d3 --- /dev/null +++ b/etc/coq/queryreplace.v @@ -0,0 +1,42 @@ +(* + +BTW, there's something stange I've forgot to post. + +In FSF-emacs PG & global-font-lock-mode does not play well together. Add + +(global-font-lock-mode t) + +in your .emacs an then try to query-replace "dom" by "foo" in + +*) + +Record t : Type := make { + dom : Set; + null : dom; + inv : dom->dom; + op : dom->dom->dom; + null_l : (x:dom)x=(op null x); + null_r : (x:dom)x=(op x null); + inv_l : (x:dom)null=(op (inv x) x); + inv_r : (x:dom)null=(op x (inv x)); + assoc : (x,y,z:dom)(op x (op y z))=(op (op x y) z); + inv_null : null=(inv null); + inv_inv : (x:dom)x=(inv (inv x)); + assoc_inv_l : (x,y:dom)y=(op (inv x) (op x y)); + assoc_inv_r : (x,y:dom)y=(op x (op (inv x) y)); + inv_op : (x,y:dom)(op (inv y) (inv x))=(inv (op x y)) + }. + + +(* + +assoc, assoc_inv_l, assoc_inv_r and inv_op occurences of "dom" are +replaced by "fooom" instead of "dom", quite strange is'n it ? + +Query-replacing "dom" by "bar" leads to "barom", which make me thinks +only the first letter of the pattern is replaced... + +I've seen this strange behaviour for a while, it was present in +earlier versions of PG & emacs. + +*) |