version 0.7.1

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

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index 3079b327b09ee47179f0468eb259074932810fd1..a424987a2de9dc19c1445d28aa9934223d96b3df 100644 (file)
--- 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
@@ -1133,7 +1133,7 @@ let rec fourier (s_proof,s_goal)=
              let curi,metasenv,pbo,pty = proof in
              let metano,context,ty = CicUtil.lookup_meta goal metasenv in
              apply_tactic 
-              (PrimitiveTactics.change_tac
+              (ReductionTactics.change_tac
                 ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
                 (Cic.Appl [ _not; ineq])) 
               status))
@@ -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*)
@@ -1179,7 +1179,7 @@ let rec fourier (s_proof,s_goal)=
                      |_ -> assert false)
                    in
                    let r = apply_tactic 
-                   (PrimitiveTactics.change_tac
+                   (ReductionTactics.change_tac
                       ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
                       w1) status
                    in