From c52e83c8428bcd4d49ff395c44485217944c5655 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 18 Jul 2002 20:27:05 +0000 Subject: New files. --- etc/coq/queryreplace.v | 42 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) create mode 100644 etc/coq/queryreplace.v (limited to 'etc/coq') 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. + +*) -- cgit v1.2.3