added support for goal patterns

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

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 96822d8e85af0511a90d1413a4632dfbbab522c7..f39ee677d28e66fdeaacd42f2987a2eb24040657 100644 (file)
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -184,7 +184,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
                        )
                    ])     
@@ -316,7 +316,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')