diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/coretactics.ml4 | 2 | ||||
| -rw-r--r-- | ltac/extratactics.ml4 | 10 | ||||
| -rw-r--r-- | ltac/tacintern.ml | 4 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 8 | ||||
| -rw-r--r-- | ltac/tacsubst.ml | 2 |
5 files changed, 13 insertions, 13 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 9879cfc280..321d50df38 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -310,7 +310,7 @@ let initial_atomic () = "hnf", TacReduce(Hnf,nocl); "simpl", TacReduce(Simpl (Redops.all_flags,None),nocl); "compute", TacReduce(Cbv Redops.all_flags,nocl); - "intros", TacIntroPattern []; + "intros", TacIntroPattern (false,[]); ] in let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index cc8fd53a7f..6d4ec83f87 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -130,12 +130,12 @@ let discrHyp id = Proofview.tclEVARMAP >>= fun sigma -> discr_main { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } -let injection_main c = - elimOnConstrWithHoles (injClause None) false c +let injection_main with_evars c = + elimOnConstrWithHoles (injClause None) with_evars c TACTIC EXTEND injection_main | [ "injection" constr_with_bindings(c) ] -> - [ injection_main c ] + [ injection_main false c ] END TACTIC EXTEND injection | [ "injection" ] -> [ injClause None false None ] @@ -144,7 +144,7 @@ TACTIC EXTEND injection END TACTIC EXTEND einjection_main | [ "einjection" constr_with_bindings(c) ] -> - [ elimOnConstrWithHoles (injClause None) true c ] + [ injection_main true c ] END TACTIC EXTEND einjection | [ "einjection" ] -> [ injClause None true None ] @@ -173,7 +173,7 @@ END let injHyp id = Proofview.tclEVARMAP >>= fun sigma -> - injection_main { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } + injection_main false { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } TACTIC EXTEND dependent_rewrite | [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ] diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index dc21fa8856..79240d2e78 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -479,8 +479,8 @@ let clause_app f = function let rec intern_atomic lf ist x = match (x:raw_atomic_tactic_expr) with (* Basic tactics *) - | TacIntroPattern l -> - TacIntroPattern (List.map (intern_intro_pattern lf ist) l) + | TacIntroPattern (ev,l) -> + TacIntroPattern (ev,List.map (intern_intro_pattern lf ist) l) | TacApply (a,ev,cb,inhyp) -> TacApply (a,ev,List.map (intern_constr_with_bindings_arg ist) cb, Option.map (intern_in_hyp_as ist lf) inhyp) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 4a33549f94..a418a624f9 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1644,17 +1644,17 @@ and name_atomic ?env tacexpr tac : unit Proofview.tactic = and interp_atomic ist tac : unit Proofview.tactic = match tac with (* Basic tactics *) - | TacIntroPattern l -> + | TacIntroPattern (ev,l) -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in - Tacticals.New.tclWITHHOLES false + Tacticals.New.tclWITHHOLES ev (name_atomic ~env - (TacIntroPattern l) + (TacIntroPattern (ev,l)) (* spiwack: print uninterpreted, not sure if it is the expected behaviour. *) - (Tactics.intro_patterns l')) sigma + (Tactics.intro_patterns ev l')) sigma end } | TacApply (a,ev,cb,cl) -> (* spiwack: until the tactic is in the monad *) diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 93c5b99555..8cb07e1c22 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -136,7 +136,7 @@ let rec subst_match_goal_hyps subst = function let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Basic tactics *) - | TacIntroPattern l -> TacIntroPattern (List.map (subst_intro_pattern subst) l) + | TacIntroPattern (ev,l) -> TacIntroPattern (ev,List.map (subst_intro_pattern subst) l) | TacApply (a,ev,cb,cl) -> TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,cl) | TacElim (ev,cb,cbo) -> |