X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FdiscriminationTactics.ml;h=24ab511f05d71c77f08e83e186b8be41f67f27d2;hb=bbe7741f3bbaacb93f2876c018dace82f5e929b8;hp=f39ee677d28e66fdeaacd42f2987a2eb24040657;hpb=abd9e5cfa8e7b6923e0664a4813a0a842f5c4e76;p=helm.git

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index f39ee677d..24ab511f0 100644
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -165,6 +165,7 @@ and injection1_tac ~term ~i =
                             ProofEngineTypes.apply_tactic 
                             (P.change_tac
                                ~what:new_t1'
+                               ~pattern:([],None)
                                ~with_what:
                                  (C.Appl [
                                    C.Lambda (
@@ -300,6 +301,7 @@ let discriminate'_tac ~term =
                              ~start:
                               (P.change_tac 
                                ~what:gty' 
+                               ~pattern:([],None)
                                ~with_what:
                                 (C.Appl [
                                   C.Lambda (