X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FfourierR.ml;h=1c4e40ed3601fa3dbeab5d2cf910ebffca3f93d2;hb=25ec5b95fe67bbdee888a8268b3772a394cd74a5;hp=3079b327b09ee47179f0468eb259074932810fd1;hpb=6cf15c86b051582032c794f7da8a325e31fc0480;p=helm.git

diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index 3079b327b..1c4e40ed3 100644
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.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))
@@ -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