Much ado about nothing:

[helm.git] / components / tactics / fourierR.ml

diff --git a/components/tactics/fourierR.ml b/components/tactics/fourierR.ml
index 4d4f305ae5684d134df97b137e3e7f90afb66c07..d9f0ce9a48f25e8eb9737ef51548b765dca72b30 100644 (file)
--- a/components/tactics/fourierR.ml
+++ b/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_