X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FfourierR.ml;h=c51d3bf0cf77e611690355ead5841272bbdd9960;hb=7b78ae643999aa95b95b376fab54adb33dbed206;hp=2ee088edbaf551c19239c51a2aab496a6b1dc8c4;hpb=abd9e5cfa8e7b6923e0664a4813a0a842f5c4e76;p=helm.git

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