From cbd0e7fdfc8d92c99cb4af414e2855400423ba73 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 18 Jul 2002 21:12:36 +0000 Subject: Investigation of proof-zap-commas failure in GNU Emacs; comments, no results. --- etc/coq/queryreplace.v | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'etc/coq') 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)) }. -- cgit v1.2.3