New files.

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.
+ 
+*)