X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FdiscriminationTactics.ml;h=a26895e6221fe003849d6597c038e37afd6263a1;hb=33a02e0b639217093eb63f30169aaa6ac8c78907;hp=21fc2b33c1f60aa1d1ded2a76fa812a4992ea97e;hpb=b8ac0d11d5cd4083838a3848fce68683a518b54a;p=helm.git

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 21fc2b33c..a26895e62 100644
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -162,21 +162,18 @@ and injection1_tac ~term ~i =
                            in
                             ProofEngineTypes.apply_tactic 
                             (ReductionTactics.change_tac
-                               ~pattern:(ProofEngineTypes.conclusion_pattern (Some new_t1'))
-                               (C.Appl [
-                                 C.Lambda (
-                                  C.Name "x", tty,
-                                  C.MutCase (
-                                   turi, typeno,
-                                   (C.Lambda (
-                                    (C.Name "x"),
+                               ~pattern:(ProofEngineTypes.conclusion_pattern
+                                (Some new_t1'))
+                               (fun _ m u ->
+                                 C.Appl [ C.Lambda (C.Name "x", tty,
+                                  C.MutCase (turi, typeno,
+                                   (C.Lambda ((C.Name "x"),
                                     (S.lift 1 tty),
                                     (S.lift 2 tty'))),
                                    (C.Rel 1), pattern
                                   )
                                  );
-                                 t1]
-                               ))
+                                 t1], m, u))
                         status
                        ))
                      ~continuation:
@@ -276,8 +273,8 @@ let discriminate'_tac ~term =
                                     C.Lambda (binder,source,(aux target (k+1)))
                                  | _ -> 
                                     if (id = false_constr_id)
-                                     then (C.MutInd(LibraryObjects.false_URI,0,[]))
-                                     else (C.MutInd(LibraryObjects.true_URI,0,[]))
+                                     then (C.MutInd(LibraryObjects.false_URI (),0,[]))
+                                     else (C.MutInd(LibraryObjects.true_URI (),0,[]))
                                in aux red_ty 1
                             ) 
                             constructor_list
@@ -287,7 +284,7 @@ let discriminate'_tac ~term =
                     let (proof',goals') = 
 		     ProofEngineTypes.apply_tactic 
                       (EliminationTactics.elim_type_tac 
-                       ~term:(C.MutInd(LibraryObjects.false_URI,0,[])))
+                       (C.MutInd(LibraryObjects.false_URI (),0,[])))
                       status 
                     in
                      (match goals' with
@@ -300,8 +297,9 @@ let discriminate'_tac ~term =
                             (T.then_
                              ~start:
                               (ReductionTactics.change_tac 
-                               ~pattern:(ProofEngineTypes.conclusion_pattern (Some gty'))
-                               (C.Appl [
+                               ~pattern:(ProofEngineTypes.conclusion_pattern
+                                (Some gty'))
+                               (fun _ m u -> C.Appl [
                                  C.Lambda (
                                   C.Name "x", tty, 
                                   C.MutCase (
@@ -310,9 +308,7 @@ let discriminate'_tac ~term =
                                    (C.Rel 1), pattern
                                   )
                                  ); 
-                                 t2]
-                               )
-                              )
+                                 t2], m, u))
                              ~continuation:
                               (
                                  T.then_