1. new syntax for patterns:

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

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index c5815471a67880622c20026a99a2e92f858042ec..07cdd5bfe7c77586e800a7a812e4f1d10bfedb26 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -586,7 +586,8 @@ let elim_intros_simpl_tac ~term =
    (Tacticals.thens
      ~start:(intros_tac ())
      ~continuations:
-       [ReductionTactics.simpl_tac ~pattern:ProofEngineTypes.goal_pattern])
+       [ReductionTactics.simpl_tac
+         ~pattern:(ProofEngineTypes.conclusion_pattern None)])
 ;;
 
 exception NotConvertible
@@ -595,7 +596,7 @@ exception NotConvertible
 (*CSC: while [what] can have a richer context (because of binders)           *)
 (*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *)
 (*CSC: Is that evident? Is that right? Or should it be changed?              *)
-let change_tac ~what ~with_what ~pattern =
+let change_tac ~pattern with_what  =
 (*
   let change_tac ~what ~with_what ~pattern (proof, goal) =
     let curi,metasenv,pbo,pty = proof in