added support for goal patterns

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

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index c155d81cc1115248fbc3597c8b8aa5824e93db76..2f1d7be47de43c0ef3d36e8b5bd5a7a372b56761 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -586,7 +586,7 @@ let elim_intros_simpl_tac ~term =
    (Tacticals.thens
      ~start:(intros_tac ())
      ~continuations:
-       [ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None])
+       [ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern])
 ;;
 
 exception NotConvertible