diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-07-18 21:12:36 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-07-18 21:12:36 +0000 |
| commit | cbd0e7fdfc8d92c99cb4af414e2855400423ba73 (patch) | |
| tree | 367732f49affb0fc0d8f9e4051365748134e140b /etc/coq | |
| parent | 58e084a35ca9930035496f21f21783ff9d9a1f12 (diff) | |
Investigation of proof-zap-commas failure in GNU Emacs; comments, no results.
Diffstat (limited to 'etc/coq')
| -rw-r--r-- | etc/coq/queryreplace.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/etc/coq/queryreplace.v b/etc/coq/queryreplace.v index cbe8e13f..d368d013 100644 --- a/etc/coq/queryreplace.v +++ b/etc/coq/queryreplace.v @@ -1,5 +1,6 @@ (* STATUS: Solved. This was caused by the anyway faulty proof-zap-commas-region failing to save the match data. + See comments in proof-syntax.el about that function. *) (* @@ -27,11 +28,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)) }. |