- tactics:

[helm.git] / components / tactics / discriminationTactics.ml

diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml
index 9c5d002ca2720a3f3aecb0531f1cba705301d146..ebf7728449dad2d03de6b08744529171c667ae34 100644 (file)
--- a/components/tactics/discriminationTactics.ml
+++ b/components/tactics/discriminationTactics.ml
@@ -186,7 +186,7 @@ let discriminate_tac ~term =
                    (EqualityTactics.rewrite_simpl_tac
                      ~direction:`RightToLeft
                      ~pattern:(ProofEngineTypes.conclusion_pattern None)
-                     term)
+                     term [])
                  ~continuation:
                    (IntroductionTactics.constructor_tac ~n:1)))) status
     | _ -> fail "not an equality"
@@ -459,7 +459,7 @@ and injection1_tac ~term ~i ~liftno ~continuation =
                              (EqualityTactics.rewrite_simpl_tac
                                ~direction:`LeftToRight
                                ~pattern:(ProofEngineTypes.conclusion_pattern None)
-                               term)
+                               term [])
                            ~continuation:EqualityTactics.reflexivity_tac)
                    ])     
                   status