X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FdiscriminationTactics.ml;h=901540b6f63685eb69c635ab15fe9a247e3b87b0;hb=25ec5b95fe67bbdee888a8268b3772a394cd74a5;hp=ffc6a9e8176889059623bdb1ae259e5227d5f255;hpb=6cf15c86b051582032c794f7da8a325e31fc0480;p=helm.git

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index ffc6a9e81..901540b6f 100644
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -163,7 +163,7 @@ and injection1_tac ~term ~i =
                              | _ -> raise (ProofEngineTypes.Fail "Injection: goal after cut is not correct")
                            in
                             ProofEngineTypes.apply_tactic 
-                            (P.change_tac
+                            (ReductionTactics.change_tac
                                ~pattern:(ProofEngineTypes.conclusion_pattern (Some new_t1'))
                                (C.Appl [
                                  C.Lambda (
@@ -301,7 +301,7 @@ let discriminate'_tac ~term =
 			    ProofEngineTypes.apply_tactic
                             (T.then_
                              ~start:
-                              (P.change_tac 
+                              (ReductionTactics.change_tac 
                                ~pattern:(ProofEngineTypes.conclusion_pattern (Some gty'))
                                (C.Appl [
                                  C.Lambda (