X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FfourierR.ml;h=a424987a2de9dc19c1445d28aa9934223d96b3df;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=1c4e40ed3601fa3dbeab5d2cf910ebffca3f93d2;hpb=25ec5b95fe67bbdee888a8268b3772a394cd74a5;p=helm.git

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index 1c4e40ed3..a424987a2 100644
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -915,7 +915,7 @@ let assumption_tac (proof,goal)=
         )  
           context 
   in
-  Tacticals.try_tactics ~tactics:tac_list (proof,goal)
+  Tacticals.first ~tactics:tac_list (proof,goal)
 ;;
 *)
 (* Galla: moved in negationTactics.ml
@@ -1162,7 +1162,7 @@ let rec fourier (s_proof,s_goal)=
                    r))
                  ~continuations:
                    [PrimitiveTactics.apply_tac ~term:_Rinv_R1;
-		    Tacticals.try_tactics 
+		    Tacticals.first 
                      ~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac] 
                    ])
                ;(*Tacticals.id_tac*)