aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/tacexpr.mli2
-rw-r--r--ltac/coretactics.ml42
-rw-r--r--ltac/extratactics.ml410
-rw-r--r--ltac/tacintern.ml4
-rw-r--r--ltac/tacinterp.ml8
-rw-r--r--ltac/tacsubst.ml2
-rw-r--r--parsing/g_tactic.ml46
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--printing/pptactic.ml9
-rw-r--r--tactics/elim.ml4
-rw-r--r--tactics/elim.mli2
-rw-r--r--tactics/equality.ml18
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/tactics.ml113
-rw-r--r--tactics/tactics.mli10
15 files changed, 101 insertions, 93 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index c0677d5e2a..35e6a2e317 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -144,7 +144,7 @@ type intro_pattern_naming = intro_pattern_naming_expr located
type 'a gen_atomic_tactic_expr =
(* Basic tactics *)
- | TacIntroPattern of 'dtrm intro_pattern_expr located list
+ | TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr located list
| TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
('nam * 'dtrm intro_pattern_expr located option) option
| TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
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) ->
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 024b51941d..a8a88d33f4 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -521,9 +521,11 @@ GEXTEND Gram
[ [
(* Basic tactics *)
IDENT "intros"; pl = ne_intropatterns ->
- TacAtom (!@loc, TacIntroPattern pl)
+ TacAtom (!@loc, TacIntroPattern (false,pl))
| IDENT "intros" ->
- TacAtom (!@loc, TacIntroPattern [!@loc,IntroForthcoming false])
+ TacAtom (!@loc, TacIntroPattern (false,[!@loc,IntroForthcoming false]))
+ | IDENT "eintros"; pl = ne_intropatterns ->
+ TacAtom (!@loc, TacIntroPattern (true,pl))
| IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (true,false,cl,inhyp))
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 94530bfde2..1ff254f6ca 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -365,7 +365,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
observe_tac("h_intro_patterns ") (let l = (List.nth intro_pats (pred i)) in
match l with
| [] -> tclIDTAC
- | _ -> Proofview.V82.of_tactic (intro_patterns l));
+ | _ -> Proofview.V82.of_tactic (intro_patterns false l));
(* unfolding of all the defined variables introduced by this branch *)
(* observe_tac "unfolding" pre_tac; *)
(* $zeta$ normalizing of the conclusion *)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index f8b34e2498..bc39c93041 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -845,17 +845,18 @@ module Make
(* Printing tactics as arguments *)
let rec pr_atom0 a = tag_atom a (match a with
- | TacIntroPattern [] -> primitive "intros"
+ | TacIntroPattern (false,[]) -> primitive "intros"
+ | TacIntroPattern (true,[]) -> primitive "eintros"
| t -> str "(" ++ pr_atom1 t ++ str ")"
)
(* Main tactic printer *)
and pr_atom1 a = tag_atom a (match a with
(* Basic tactics *)
- | TacIntroPattern [] as t ->
+ | TacIntroPattern (ev,[]) as t ->
pr_atom0 t
- | TacIntroPattern (_::_ as p) ->
- hov 1 (primitive "intros" ++ spc () ++
+ | TacIntroPattern (ev,(_::_ as p)) ->
+ hov 1 (primitive (if ev then "eintros" else "intros") ++ spc () ++
prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
| TacApply (a,ev,cb,inhyp) ->
hov 1 (
diff --git a/tactics/elim.ml b/tactics/elim.ml
index d59c2fba49..f2b9eec4b2 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -25,14 +25,14 @@ let introElimAssumsThen tac ba =
(tclTHEN introElimAssums (elim_on_ba tac ba))
(* Supposed to be called with a non-recursive scheme *)
-let introCaseAssumsThen tac ba =
+let introCaseAssumsThen with_evars tac ba =
let n1 = List.length ba.Tacticals.branchsign in
let n2 = List.length ba.Tacticals.branchnames in
let (l1,l2),l3 =
if n1 < n2 then List.chop n1 ba.Tacticals.branchnames, []
else (ba.Tacticals.branchnames, []), List.make (n1-n2) false in
let introCaseAssums =
- tclTHEN (intro_patterns l1) (intros_clearing l3) in
+ tclTHEN (intro_patterns with_evars l1) (intros_clearing l3) in
(tclTHEN introCaseAssums (case_on_ba (tac l2) ba))
(* The following tactic Decompose repeatedly applies the
diff --git a/tactics/elim.mli b/tactics/elim.mli
index a94f642a07..ae9cf85f3c 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -13,7 +13,7 @@ open Misctypes
(** Eliminations tactics. *)
-val introCaseAssumsThen :
+val introCaseAssumsThen : Tacexpr.evars_flag ->
(Tacexpr.intro_patterns -> branch_assumptions -> unit Proofview.tactic) ->
branch_args -> unit Proofview.tactic
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 12d31d0f31..db7d2e4a13 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1383,7 +1383,7 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
let use_clear_hyp_by_default () = false
-let postInjEqTac clear_flag ipats c n =
+let postInjEqTac with_evars clear_flag ipats c n =
match ipats with
| Some ipats ->
let clear_tac =
@@ -1392,21 +1392,21 @@ let postInjEqTac clear_flag ipats c n =
tclTRY (apply_clear_request clear_flag dft c) in
let intro_tac =
if use_injection_pattern_l2r_order ()
- then intro_patterns_bound_to n MoveLast ipats
- else intro_patterns_to MoveLast ipats in
+ then intro_patterns_bound_to with_evars n MoveLast ipats
+ else intro_patterns_to with_evars MoveLast ipats in
tclTHEN clear_tac intro_tac
| None -> apply_clear_request clear_flag false c
-let injEq clear_flag ipats =
+let injEq with_evars clear_flag ipats =
let l2r =
if use_injection_pattern_l2r_order () && not (Option.is_empty ipats) then true else false
in
- injEqThen (fun c i -> postInjEqTac clear_flag ipats c i) l2r
+ injEqThen (fun c i -> postInjEqTac with_evars clear_flag ipats c i) l2r
-let inj ipats with_evars clear_flag = onEquality with_evars (injEq clear_flag ipats)
+let inj ipats with_evars clear_flag = onEquality with_evars (injEq with_evars clear_flag ipats)
let injClause ipats with_evars = function
- | None -> onNegatedEquality with_evars (injEq None ipats)
+ | None -> onNegatedEquality with_evars (injEq with_evars None ipats)
| Some c -> onInductionArg (inj ipats with_evars) c
let injConcl = injClause None false None
@@ -1434,13 +1434,13 @@ let dEq with_evars =
dEqThen with_evars (fun clear_flag c x ->
(apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
-let intro_decompe_eq tac data cl =
+let intro_decomp_eq tac data cl =
Proofview.Goal.enter { enter = begin fun gl ->
let cl = pf_apply make_clenv_binding gl cl NoBindings in
decompEqThen (fun _ -> tac) data cl
end }
-let _ = declare_intro_decomp_eq intro_decompe_eq
+let _ = declare_intro_decomp_eq intro_decomp_eq
(* [subst_tuple_term dep_pair B]
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 3707ef90b4..852c2ee7cb 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -465,7 +465,7 @@ let raw_inversion inv_kind id status names =
(tclTHENS
(assert_before Anonymous cut_concl)
[case_tac names
- (introCaseAssumsThen
+ (introCaseAssumsThen false (* ApplyOn not supported by inversion *)
(rewrite_equations_tac as_mode inv_kind id neqns))
(Some elim_predicate) ind (c, t);
onLastHypId (fun id -> tclTHEN (refined id) reflexivity)])
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2f24e55a57..61a0850c27 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1416,6 +1416,7 @@ let general_case_analysis with_evars clear_flag (c,lbindc as cx) =
general_case_analysis_in_context with_evars clear_flag cx
let simplest_case c = general_case_analysis false None (c,NoBindings)
+let simplest_ecase c = general_case_analysis true None (c,NoBindings)
(* Elimination tactic with bindings but using the default elimination
* constant associated with the type. *)
@@ -2241,7 +2242,7 @@ let intro_decomp_eq loc l thin tac id =
Tacticals.New.tclZEROMSG (str "Not a primitive equality here.")
end }
-let intro_or_and_pattern loc bracketed ll thin tac id =
+let intro_or_and_pattern loc with_evars bracketed ll thin tac id =
Proofview.Goal.enter { enter = begin fun gl ->
let c = mkVar id in
let t = Tacmach.New.pf_unsafe_type_of gl c in
@@ -2251,14 +2252,14 @@ let intro_or_and_pattern loc bracketed ll thin tac id =
let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in
let ll = get_and_check_or_and_pattern loc ll branchsigns in
Tacticals.New.tclTHENLASTn
- (Tacticals.New.tclTHEN (simplest_case c) (clear [id]))
+ (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id]))
(Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
nv_with_let ll)
end }
-let rewrite_hyp_then assert_style thin l2r id tac =
+let rewrite_hyp_then assert_style with_evars thin l2r id tac =
let rew_on l2r =
- Hook.get forward_general_rewrite_clause l2r false (mkVar id,NoBindings) in
+ Hook.get forward_general_rewrite_clause l2r with_evars (mkVar id,NoBindings) in
let subst_on l2r x rhs =
Hook.get forward_subst_one true x (id,rhs,l2r) in
let clear_var_and_eq id' = clear [id';id] in
@@ -2369,12 +2370,13 @@ let exceed_bound n = function
[patl]: introduction patterns to interpret
*)
-let rec intro_patterns_core b avoid ids thin destopt bound n tac = function
+let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac =
+ function
| [] when fit_bound n bound ->
tac ids thin
| [] ->
(* Behave as IntroAnonymous *)
- intro_patterns_core b avoid ids thin destopt bound n tac
+ intro_patterns_core with_evars b avoid ids thin destopt bound n tac
[dloc,IntroNaming IntroAnonymous]
| (loc,pat) :: l ->
if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else
@@ -2382,48 +2384,49 @@ let rec intro_patterns_core b avoid ids thin destopt bound n tac = function
| IntroForthcoming onlydeps ->
intro_forthcoming_then_gen (NamingAvoid (avoid@explicit_intro_names l))
destopt onlydeps n bound
- (fun ids -> intro_patterns_core b avoid ids thin destopt bound
+ (fun ids -> intro_patterns_core with_evars b avoid ids thin destopt bound
(n+List.length ids) tac l)
| IntroAction pat ->
intro_then_gen (make_tmp_naming avoid l pat)
destopt true false
- (intro_pattern_action loc (b || not (List.is_empty l)) false pat thin
- destopt
- (fun thin bound' -> intro_patterns_core b avoid ids thin destopt bound' 0
+ (intro_pattern_action loc with_evars (b || not (List.is_empty l)) false
+ pat thin destopt
+ (fun thin bound' -> intro_patterns_core with_evars b avoid ids thin destopt bound' 0
(fun ids thin ->
- intro_patterns_core b avoid ids thin destopt bound (n+1) tac l)))
+ intro_patterns_core with_evars b avoid ids thin destopt bound (n+1) tac l)))
| IntroNaming pat ->
- intro_pattern_naming loc b avoid ids pat thin destopt bound (n+1) tac l
+ intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound (n+1) tac l
(* Pi-introduction rule, used backwards *)
-and intro_pattern_naming loc b avoid ids pat thin destopt bound n tac l =
+and intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound n tac l =
match pat with
| IntroIdentifier id ->
check_thin_clash_then id thin avoid (fun thin ->
intro_then_gen (NamingMustBe (loc,id)) destopt true false
- (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l))
+ (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l))
| IntroAnonymous ->
intro_then_gen (NamingAvoid (avoid@explicit_intro_names l))
destopt true false
- (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l)
+ (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)
| IntroFresh id ->
(* todo: avoid thinned names to interfere with generation of fresh name *)
intro_then_gen (NamingBasedOn (id, avoid@explicit_intro_names l))
destopt true false
- (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l)
+ (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)
-and intro_pattern_action loc b style pat thin destopt tac id = match pat with
+and intro_pattern_action loc with_evars b style pat thin destopt tac id =
+ match pat with
| IntroWildcard ->
tac ((loc,id)::thin) None []
| IntroOrAndPattern ll ->
- intro_or_and_pattern loc b ll thin tac id
+ intro_or_and_pattern loc with_evars b ll thin tac id
| IntroInjection l' ->
intro_decomp_eq loc l' thin tac id
| IntroRewrite l2r ->
- rewrite_hyp_then style thin l2r id (fun thin -> tac thin None [])
+ rewrite_hyp_then style with_evars thin l2r id (fun thin -> tac thin None [])
| IntroApplyOn (f,(loc,pat)) ->
let naming,tac_ipat =
- prepare_intros_loc loc (IntroIdentifier id) destopt pat in
+ prepare_intros_loc loc with_evars (IntroIdentifier id) destopt pat in
let doclear =
if naming = NamingMustBe (loc,id) then
Proofview.tclUNIT () (* apply_in_once do a replacement *)
@@ -2433,48 +2436,48 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
let Sigma (c, sigma, p) = f.delayed env sigma in
Sigma ((c, NoBindings), sigma, p)
} in
- apply_in_delayed_once false true true true naming id (None,(loc,f))
+ apply_in_delayed_once false true true with_evars naming id (None,(loc,f))
(fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []])
-and prepare_intros_loc loc dft destopt = function
+and prepare_intros_loc loc with_evars dft destopt = function
| IntroNaming ipat ->
prepare_naming loc ipat,
(fun id -> move_hyp id destopt)
| IntroAction ipat ->
prepare_naming loc dft,
(let tac thin bound =
- intro_patterns_core true [] [] thin destopt bound 0
+ intro_patterns_core with_evars true [] [] thin destopt bound 0
(fun _ l -> clear_wildcards l) in
- fun id -> intro_pattern_action loc true true ipat [] destopt tac id)
+ fun id ->
+ intro_pattern_action loc with_evars true true ipat [] destopt tac id)
| IntroForthcoming _ -> user_err_loc
(loc,"",str "Introduction pattern for one hypothesis expected.")
-let intro_patterns_bound_to n destopt =
- intro_patterns_core true [] [] [] destopt
+let intro_patterns_bound_to with_evars n destopt =
+ intro_patterns_core with_evars true [] [] [] destopt
(Some (true,n)) 0 (fun _ l -> clear_wildcards l)
-let intro_patterns_to destopt l =
- (* Eta-expansion because of a side-effect *)
- intro_patterns_core (use_bracketing_last_or_and_intro_pattern ())
- [] [] [] destopt None 0 (fun _ l -> clear_wildcards l) l
+let intro_patterns_to with_evars destopt =
+ intro_patterns_core with_evars (use_bracketing_last_or_and_intro_pattern ())
+ [] [] [] destopt None 0 (fun _ l -> clear_wildcards l)
-let intro_pattern_to destopt pat =
- intro_patterns_to destopt [dloc,pat]
+let intro_pattern_to with_evars destopt pat =
+ intro_patterns_to with_evars destopt [dloc,pat]
-let intro_patterns = intro_patterns_to MoveLast
+let intro_patterns with_evars = intro_patterns_to with_evars MoveLast
(* Implements "intros" *)
-let intros_patterns = function
+let intros_patterns with_evars = function
| [] -> intros
- | l -> intro_patterns_to MoveLast l
+ | l -> intro_patterns_to with_evars MoveLast l
(**************************)
(* Forward reasoning *)
(**************************)
-let prepare_intros dft destopt = function
+let prepare_intros with_evars dft destopt = function
| None -> prepare_naming dloc dft, (fun _id -> Proofview.tclUNIT ())
- | Some (loc,ipat) -> prepare_intros_loc loc dft destopt ipat
+ | Some (loc,ipat) -> prepare_intros_loc loc with_evars dft destopt ipat
let ipat_of_name = function
| Anonymous -> None
@@ -2485,7 +2488,7 @@ let head_ident c =
if isVar c then Some (destVar c) else None
let assert_as first hd ipat t =
- let naming,tac = prepare_intros IntroAnonymous MoveLast ipat in
+ let naming,tac = prepare_intros false IntroAnonymous MoveLast ipat in
let repl = do_replace hd naming in
let tac = if repl then (fun id -> Proofview.tclUNIT ()) else tac in
if first then assert_before_then_gen repl naming t tac
@@ -2502,7 +2505,8 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
let destopt =
if with_evars then MoveLast (* evars would depend on the whole context *)
else get_previous_hyp_position id gl in
- let naming,ipat_tac = prepare_intros (IntroIdentifier id) destopt ipat in
+ let naming,ipat_tac =
+ prepare_intros with_evars (IntroIdentifier id) destopt ipat in
let lemmas_target, last_lemma_target =
let last,first = List.sep_last lemmas in
List.map (fun lem -> (NamingMustBe (dloc,id),lem)) first, (naming,last)
@@ -2979,19 +2983,19 @@ let re_intro_dependent_hypotheses (lstatus,rstatus) (_,tophyp) =
(intros_move rstatus)
(intros_move newlstatus)
-let dest_intro_patterns avoid thin dest pat tac =
- intro_patterns_core true avoid [] thin dest None 0 tac pat
+let dest_intro_patterns with_evars avoid thin dest pat tac =
+ intro_patterns_core with_evars true avoid [] thin dest None 0 tac pat
-let safe_dest_intro_patterns avoid thin dest pat tac =
+let safe_dest_intro_patterns with_evars avoid thin dest pat tac =
Proofview.tclORELSE
- (dest_intro_patterns avoid thin dest pat tac)
+ (dest_intro_patterns with_evars avoid thin dest pat tac)
begin function (e, info) -> match e with
| UserError ("move_hyp",_) ->
(* May happen e.g. with "destruct x using s" with an hypothesis
which is morally an induction hypothesis to be "MoveLast" if
known as such but which is considered instead as a subterm of
a constructor to be move at the place of x. *)
- dest_intro_patterns avoid thin MoveLast pat tac
+ dest_intro_patterns with_evars avoid thin MoveLast pat tac
| e -> Proofview.tclZERO ~info e
end
@@ -3023,7 +3027,7 @@ let get_recarg_dest (recargdests,tophyp) =
had to be introduced at the top of the context).
*)
-let induct_discharge dests avoid' tac (avoid,ra) names =
+let induct_discharge with_evars dests avoid' tac (avoid,ra) names =
let avoid = avoid @ avoid' in
let rec peel_tac ra dests names thin =
match ra with
@@ -3036,12 +3040,12 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
(pat, [dloc, IntroNaming (IntroIdentifier id')])
| _ -> consume_pattern avoid (Name recvarname) deprec gl names in
let dest = get_recarg_dest dests in
- dest_intro_patterns avoid thin dest [recpat] (fun ids thin ->
+ dest_intro_patterns with_evars avoid thin dest [recpat] (fun ids thin ->
Proofview.Goal.enter { enter = begin fun gl ->
let (hyprec,names) =
consume_pattern avoid (Name hyprecname) depind gl names
in
- dest_intro_patterns avoid thin MoveLast [hyprec] (fun ids' thin ->
+ dest_intro_patterns with_evars avoid thin MoveLast [hyprec] (fun ids' thin ->
peel_tac ra' (update_dest dests ids') names thin)
end })
end }
@@ -3050,7 +3054,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
let pat,names =
consume_pattern avoid (Name hyprecname) dep gl names in
- dest_intro_patterns avoid thin MoveLast [pat] (fun ids thin ->
+ dest_intro_patterns with_evars avoid thin MoveLast [pat] (fun ids thin ->
peel_tac ra' (update_dest dests ids) names thin)
end }
| (RecArg,_,dep,recvarname) :: ra' ->
@@ -3058,14 +3062,14 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
let (pat,names) =
consume_pattern avoid (Name recvarname) dep gl names in
let dest = get_recarg_dest dests in
- dest_intro_patterns avoid thin dest [pat] (fun ids thin ->
+ dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin ->
peel_tac ra' dests names thin)
end }
| (OtherArg,_,dep,_) :: ra' ->
Proofview.Goal.enter { enter = begin fun gl ->
let (pat,names) = consume_pattern avoid Anonymous dep gl names in
let dest = get_recarg_dest dests in
- safe_dest_intro_patterns avoid thin dest [pat] (fun ids thin ->
+ safe_dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin ->
peel_tac ra' dests names thin)
end }
| [] ->
@@ -4052,7 +4056,7 @@ let induction_tac with_evars params indvars elim =
hypotheses from the context, replacing the main hypothesis on which
induction applies with the induction hypotheses *)
-let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac =
+let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_tac =
let open Context.Named.Declaration in
Proofview.Goal.s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
@@ -4082,7 +4086,8 @@ let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac =
Tacticals.New.tclMAP expand_hyp toclear;
])
(Array.map2
- (induct_discharge lhyp0 avoid (re_intro_dependent_hypotheses statuslists))
+ (induct_discharge with_evars lhyp0 avoid
+ (re_intro_dependent_hypotheses statuslists))
indsign names)
in
Sigma.Unsafe.of_pair (tac, sigma)
@@ -4092,7 +4097,7 @@ let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyp
Proofview.Goal.enter { enter = begin fun gl ->
let elim_info = find_induction_type isrec elim hyp0 (Proofview.Goal.assume gl) in
atomize_param_of_ind_then elim_info hyp0 (fun indvars ->
- apply_induction_in_context (Some hyp0) inhyps (pi3 elim_info) indvars names
+ apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names
(fun elim -> induction_tac with_evars [] [hyp0] elim))
end }
@@ -4141,7 +4146,7 @@ let induction_without_atomization isrec with_evars elim names lid =
induction_tac with_evars params realindvars elim;
] in
let elim = ElimUsing (({elimindex = Some (-1); elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in
- apply_induction_in_context None [] elim indvars names induct_tac
+ apply_induction_in_context with_evars None [] elim indvars names induct_tac
end }
(* assume that no occurrences are selected *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 142fdd3ebc..e346a0d566 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -102,16 +102,16 @@ val use_clear_hyp_by_default : unit -> bool
(** {6 Introduction tactics with eliminations. } *)
-val intro_patterns : intro_patterns -> unit Proofview.tactic
-val intro_patterns_to : Id.t move_location -> intro_patterns ->
+val intro_patterns : evars_flag -> intro_patterns -> unit Proofview.tactic
+val intro_patterns_to : evars_flag -> Id.t move_location -> intro_patterns ->
unit Proofview.tactic
-val intro_patterns_bound_to : int -> Id.t move_location -> intro_patterns ->
+val intro_patterns_bound_to : evars_flag -> int -> Id.t move_location -> intro_patterns ->
unit Proofview.tactic
-val intro_pattern_to : Id.t move_location -> delayed_open_constr intro_pattern_expr ->
+val intro_pattern_to : evars_flag -> Id.t move_location -> delayed_open_constr intro_pattern_expr ->
unit Proofview.tactic
(** Implements user-level "intros", with [] standing for "**" *)
-val intros_patterns : intro_patterns -> unit Proofview.tactic
+val intros_patterns : evars_flag -> intro_patterns -> unit Proofview.tactic
(** {6 Exact tactics. } *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-30 21:20:45 +0000