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

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 96822d8e8..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 (
@@ -184,7 +185,7 @@ and injection1_tac ~term ~i =
                        ))
                      ~continuation:
                        (T.then_
-                         ~start:(EqualityTactics.rewrite_simpl_tac ~term)
+                         ~start:(EqualityTactics.rewrite_simpl_tac ~term ())
                          ~continuation:EqualityTactics.reflexivity_tac
                        )
                    ])     
@@ -300,6 +301,7 @@ let discriminate'_tac ~term =
                              ~start:
                               (P.change_tac 
                                ~what:gty' 
+                               ~pattern:([],None)
                                ~with_what:
                                 (C.Appl [
                                   C.Lambda (
@@ -316,7 +318,8 @@ let discriminate'_tac ~term =
                              ~continuation:
                               (
                                  T.then_
-                                   ~start:(EqualityTactics.rewrite_back_simpl_tac ~term)
+                                   ~start:(EqualityTactics.rewrite_back_simpl_tac
+                                   ~term ())
                                    ~continuation:(IntroductionTactics.constructor_tac ~n:1) 
                               ))
                              (proof',goal')