diff options
-rw-r--r-- | etc/coq/queryreplace.v | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/etc/coq/queryreplace.v b/etc/coq/queryreplace.v index 977846d3..cbe8e13f 100644 --- a/etc/coq/queryreplace.v +++ b/etc/coq/queryreplace.v @@ -1,4 +1,12 @@ +(* STATUS: Solved. This was caused by the anyway faulty + proof-zap-commas-region failing to save the match data. +*) + (* +From: Cuihtlauac ALVARADO <cuihtlauac.alvarado@francetelecom.com> +To: David Aspinall <da@dcs.ed.ac.uk> +Subject: broken query-replace +Date: 09 Jul 2002 11:09:03 +0200 BTW, there's something stange I've forgot to post. @@ -19,11 +27,11 @@ Record t : Type := make { 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); + 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)); + 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)) }. |