X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FfourierR.ml;h=d9f0ce9a48f25e8eb9737ef51548b765dca72b30;hb=d3d4ea54cb895a1adc6cb327df42e1394b3f2bea;hp=4d4f305ae5684d134df97b137e3e7f90afb66c07;hpb=61a2faa2694907757dd617175e0144705e79d65a;p=helm.git

diff --git a/helm/software/components/tactics/fourierR.ml b/helm/software/components/tactics/fourierR.ml
index 4d4f305ae..d9f0ce9a4 100644
--- a/helm/software/components/tactics/fourierR.ml
+++ b/helm/software/components/tactics/fourierR.ml
@@ -1161,7 +1161,7 @@ let rec fourier (s_proof,s_goal)=
                  ~continuations:
                    [PrimitiveTactics.apply_tac ~term:_Rinv_R1;
 		    Tacticals.first 
-                     ~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac] 
+                     ~tactics:[Ring.ring_tac; Tacticals.id_tac] 
                    ])
                ;(*Tacticals.id_tac*)
                 Tacticals.then_