From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 22 Oct 2002 09:59:49 +0000 (+0000)
Subject: Bug ``fixed'': we do not need to apply sym_eqT since the goal we produce
X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~17
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b730b0cce33420d6f313d4563259e8ce4680203f;p=helm.git

Bug ``fixed'': we do not need to apply sym_eqT since the goal we produce
is already 1^-1 = 1 (while Coq produces 1 = 1^-1).
---

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index eefec1cea..0dd76f89a 100644
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -1178,6 +1178,12 @@ theoreme,so let's parse our thesis *)
 		   (match r with (p,gl) ->
 		     debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
 		   r)
+		 ~continuations:
+                   [PrimitiveTactics.apply_tac ~term:_Rinv_R1
+(* CSC: Il nostro goal e' 1^-1 = 1 e non 1 = 1^-1. Quindi non c'e' bisogno
+   di applicare sym_eqT. Perche' in Coq il goal e' al contrario? Forse i
+   parametri della equality_replace vengono passati al contrario? Oppure la
+   tattica usa i parametri al contrario?
 		 ~continuations:[Tacticals.then_ 
 		   ~start:(
 	             fun ~status:(proof,goal as status) ->
@@ -1191,6 +1197,7 @@ theoreme,so let's parse our thesis *)
 		     debug("fine ECCOCI\n");
 		     r)
 		   ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
+*)
 		 ;Tacticals.try_tactics 
 		   ~tactics:[ "ring", (fun ~status -> 
 				        debug("begin RING\n");
@@ -1199,6 +1206,7 @@ theoreme,so let's parse our thesis *)
 					r)
 			; "id", Ring.id_tac] 
 		 ])
+(* CSC: NOW THE BUG IS HERE: tac2 DOES NOT WORK ANY MORE *)
 	       ;tac2]))
 	 ;!tac1]);(*end tac:=*)
        tac:=(Tacticals.thens