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

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index e6fa4edcd..a424987a2 100644
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -693,16 +693,12 @@ let tac_zero_infeq_false gl (n,d) =
    (Tacticals.then_
     ~start:
       (ReductionTactics.fold_tac ~reduction:CicReduction.whd
-        ~pattern:
-          (ProofEngineTypes.conclusion_pattern
-            (Some
-              (Cic.Appl
-                [_Rle ; _R0 ;
-                 Cic.Appl
-                  [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
-                ]
-              )))
-      )
+        ~pattern:(ProofEngineTypes.conclusion_pattern None)
+        ~term:
+          (Cic.Appl
+            [_Rle ; _R0 ;
+              Cic.Appl
+               [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]]))
     ~continuation:
       (Tacticals.then_ 
         ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
@@ -886,7 +882,10 @@ let equality_replace a b =
     let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
  debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
     let (proof,goals) = apply_tactic 
-     (EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) ())
+     (EqualityTactics.rewrite_simpl_tac
+       ~direction:`LeftToRight
+       ~pattern:(ProofEngineTypes.conclusion_pattern None)
+       (C.Meta (fresh_meta,irl)))
      ((curi,metasenv',pbo,pty),goal)
     in
     let new_goals = fresh_meta::goals in
@@ -916,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
@@ -1134,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))
@@ -1163,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*)
@@ -1180,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