1. new syntax for patterns:

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

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index c51d3bf0cf77e611690355ead5841272bbdd9960..e6fa4edcd6275e92be398a3f358cf37a8fbcaba6 100644 (file)
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -693,14 +693,15 @@ let tac_zero_infeq_false gl (n,d) =
    (Tacticals.then_
     ~start:
       (ReductionTactics.fold_tac ~reduction:CicReduction.whd
-        ~pattern:([],None)
-        ~term:
-          (Cic.Appl
-            [_Rle ; _R0 ;
-             Cic.Appl
-              [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
-            ]
-          )
+        ~pattern:
+          (ProofEngineTypes.conclusion_pattern
+            (Some
+              (Cic.Appl
+                [_Rle ; _R0 ;
+                 Cic.Appl
+                  [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
+                ]
+              )))
       )
     ~continuation:
       (Tacticals.then_ 
@@ -1133,8 +1134,9 @@ 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 ~what:ty ~pattern:([],None)
-                ~with_what:(Cic.Appl [ _not; ineq])) 
+              (PrimitiveTactics.change_tac
+                ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
+                (Cic.Appl [ _not; ineq])) 
               status))
            ~continuation:(Tacticals.then_ 
              ~start:(PrimitiveTactics.apply_tac ~term:
@@ -1178,8 +1180,10 @@ let rec fourier (s_proof,s_goal)=
                      |_ -> assert false)
                    in
                    let r = apply_tactic 
-                   (PrimitiveTactics.change_tac ~what:ty ~pattern:([],None)
-                      ~with_what:w1) status in
+                   (PrimitiveTactics.change_tac
+                      ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
+                      w1) status
+                   in
                    debug("fine MY_CHNGE\n");
                    r)) 
                  ~continuation:(*PORTINGTacticals.id_tac*)tac2]))