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 eefec1ceacf7a68a8100a5edd086619062e7678c..0dd76f89a5a806ade2c9556b3226639014b053f5 100644 (file)
--- 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