1. rewrite_* and rewrite_back_* merged into one function

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

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 05344e0abf93d9debb2135047c297a6528d3dbab..ffc6a9e8176889059623bdb1ae259e5227d5f255 100644 (file)
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -183,7 +183,11 @@ and injection1_tac ~term ~i =
                        ))
                      ~continuation:
                        (T.then_
-                         ~start:(EqualityTactics.rewrite_simpl_tac ~term ())
+                         ~start:
+                           (EqualityTactics.rewrite_simpl_tac
+                             ~direction:`LeftToRight
+                             ~pattern:(ProofEngineTypes.conclusion_pattern None)
+                             term)
                          ~continuation:EqualityTactics.reflexivity_tac
                        )
                    ])     
@@ -314,8 +318,11 @@ let discriminate'_tac ~term =
                              ~continuation:
                               (
                                  T.then_
-                                   ~start:(EqualityTactics.rewrite_back_simpl_tac
-                                   ~term ())
+                                   ~start:
+                                     (EqualityTactics.rewrite_simpl_tac
+                                       ~direction:`RightToLeft
+                                       ~pattern:(ProofEngineTypes.conclusion_pattern None)
+                                       term)
                                    ~continuation:(IntroductionTactics.constructor_tac ~n:1) 
                               ))
                              (proof',goal')