diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-07-18 20:36:25 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-07-18 20:36:25 +0000 |
| commit | 56ccfda3f48d5ebdaf5b17269626f78514abbc46 (patch) | |
| tree | 122863455cb11ea2e6d0e6ae706d2f3541592937 /etc/coq | |
| parent | c52e83c8428bcd4d49ff395c44485217944c5655 (diff) | |
Record bug as solved.
Diffstat (limited to 'etc/coq')
| -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)) }. |