1. change_tac moved from PrimitiveTactics to ReductionTactics

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

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index 2fbba97ad5b7d905d48b8ddde2c96bf40a252136..1c4e40ed3601fa3dbeab5d2cf910ebffca3f93d2 100644 (file)
--- 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)
@@ -1137,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))
@@ -1183,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