aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/declareUctx.ml2
-rw-r--r--tactics/eqdecide.ml4
-rw-r--r--tactics/equality.ml14
-rw-r--r--tactics/equality.mli4
-rw-r--r--tactics/genredexpr.ml13
-rw-r--r--tactics/hints.ml23
-rw-r--r--tactics/redexpr.ml112
-rw-r--r--tactics/redexpr.mli10
-rw-r--r--tactics/tacticals.ml26
-rw-r--r--tactics/tacticals.mli4
-rw-r--r--tactics/tactics.ml178
-rw-r--r--tactics/tactics.mli2
12 files changed, 224 insertions, 168 deletions
diff --git a/tactics/declareUctx.ml b/tactics/declareUctx.ml
index 3f67ff20a4..6c8bc92865 100644
--- a/tactics/declareUctx.ml
+++ b/tactics/declareUctx.ml
@@ -16,7 +16,7 @@ let name_instance inst =
assert false
| Some na ->
try
- let qid = Nametab.shortest_qualid_of_universe na in
+ let qid = Nametab.shortest_qualid_of_universe Names.Id.Map.empty na in
Names.Name (Libnames.qualid_basename qid)
with Not_found ->
(* Best-effort naming from the string representation of the level.
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index d4cc193eb3..9b3f9053cd 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -123,8 +123,8 @@ let idy = Id.of_string "y"
let mkGenDecideEqGoal rectype ops g =
let hypnames = pf_ids_set_of_hyps g in
- let xname = next_ident_away idx hypnames
- and yname = next_ident_away idy hypnames in
+ let xname = next_ident_away idx hypnames in
+ let yname = next_ident_away idy (Id.Set.add xname hypnames) in
(mkNamedProd (make_annot xname Sorts.Relevant) rectype
(mkNamedProd (make_annot yname Sorts.Relevant) rectype
(mkDecideEqGoal true ops
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 486575d229..633b9da053 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -154,7 +154,8 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
let c1 = args.(arglen - 2) in
let c2 = args.(arglen - 1) in
let try_occ (evd', c') =
- Clenv.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'}
+ let clenv = Clenv.update_clenv_evd eqclause evd' in
+ Clenv.clenv_pose_dependent_evars ~with_evars:true clenv
in
let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
let occs =
@@ -1655,6 +1656,17 @@ let cutSubstClause l2r eqn cls =
| None -> cutSubstInConcl l2r eqn
| Some id -> cutSubstInHyp l2r eqn id
+let warn_deprecated_cutrewrite =
+ CWarnings.create ~name:"deprecated-cutrewrite" ~category:"deprecated"
+ (fun () -> strbrk"\"cutrewrite\" is deprecated. Use \"replace\" instead.")
+
+let cutRewriteClause l2r eqn cls =
+ warn_deprecated_cutrewrite ();
+ try_rewrite (cutSubstClause l2r eqn cls)
+
+let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
+let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
+
let substClause l2r c cls =
Proofview.Goal.enter begin fun gl ->
let eq = pf_apply get_type_of gl c in
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 5a4fe47cab..fdcbbc0e3c 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -107,6 +107,10 @@ val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -
val make_iterated_tuple :
env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr)
+(* The family cutRewriteIn expect an equality statement *)
+val cutRewriteInHyp : bool -> types -> Id.t -> unit Proofview.tactic
+val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic
+
(* The family rewriteIn expect the proof of an equality *)
val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic
val rewriteInConcl : bool -> constr -> unit Proofview.tactic
diff --git a/tactics/genredexpr.ml b/tactics/genredexpr.ml
index 1f6b04c1d3..9939490e79 100644
--- a/tactics/genredexpr.ml
+++ b/tactics/genredexpr.ml
@@ -35,13 +35,13 @@ type 'a glob_red_flag = {
(** Generic kinds of reductions *)
-type ('a,'b,'c) red_expr_gen =
+type ('a, 'b, 'c, 'flags) red_expr_gen0 =
| Red of bool
| Hnf
- | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option
- | Cbv of 'b glob_red_flag
- | Cbn of 'b glob_red_flag
- | Lazy of 'b glob_red_flag
+ | Simpl of 'flags * ('b, 'c) Util.union Locus.with_occurrences option
+ | Cbv of 'flags
+ | Cbn of 'flags
+ | Lazy of 'flags
| Unfold of 'b Locus.with_occurrences list
| Fold of 'a list
| Pattern of 'a Locus.with_occurrences list
@@ -49,6 +49,9 @@ type ('a,'b,'c) red_expr_gen =
| CbvVm of ('b,'c) Util.union Locus.with_occurrences option
| CbvNative of ('b,'c) Util.union Locus.with_occurrences option
+type ('a, 'b, 'c) red_expr_gen =
+ ('a, 'b, 'c, 'b glob_red_flag) red_expr_gen0
+
type ('a,'b,'c) may_eval =
| ConstrTerm of 'a
| ConstrEval of ('a,'b,'c) red_expr_gen * 'a
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 6fab111e6f..ace51c40d4 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -340,10 +340,8 @@ let instantiate_hint env sigma p =
let mk_clenv (c, cty, ctx) =
let sigma = merge_context_set_opt sigma ctx in
let cl = mk_clenv_from_env env sigma None (c,cty) in
- let cl = {cl with templval =
- { cl.templval with rebus = strip_params env sigma cl.templval.rebus };
- env = empty_env}
- in
+ let templval = { cl.templval with rebus = strip_params env sigma cl.templval.rebus } in
+ let cl = mk_clausenv empty_env cl.evd templval cl.templtyp in
{ hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; }
in
let code = match p.code.obj with
@@ -1649,14 +1647,17 @@ let connect_hint_clenv h gl =
let emap c = Vars.subst_univs_level_constr subst c in
let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
(* Only metas are mentioning the old universes. *)
- {
- templval = Evd.map_fl emap clenv.templval;
- templtyp = Evd.map_fl emap clenv.templtyp;
- evd = Evd.map_metas emap evd;
- env = Proofview.Goal.env gl;
- }
+ Clenv.mk_clausenv
+ (Proofview.Goal.env gl)
+ (Evd.map_metas emap evd)
+ (Evd.map_fl emap clenv.templval)
+ (Evd.map_fl emap clenv.templtyp)
| None ->
- { clenv with evd = evd ; env = Proofview.Goal.env gl }
+ Clenv.mk_clausenv
+ (Proofview.Goal.env gl)
+ evd
+ clenv.templval
+ clenv.templtyp
let fresh_hint env sigma h =
let { hint_term = c; hint_uctx = ctx } = h in
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index a8747e0a7c..9c2df71f82 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -129,6 +129,9 @@ let set_strategy local str =
type red_expr =
(constr, evaluable_global_reference, constr_pattern) red_expr_gen
+type red_expr_val =
+ (constr, evaluable_global_reference, constr_pattern, CClosure.RedFlags.reds) red_expr_gen0
+
let make_flag_constant = function
| EvalVarRef id -> fVAR id
| EvalConstRef sp -> fCONST sp
@@ -221,38 +224,117 @@ let warn_simpl_unfolding_modifiers =
(fun () ->
Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.")
-let reduction_of_red_expr env =
- let make_flag = make_flag env in
- let rec reduction_of_red_expr = function
+let rec eval_red_expr env = function
+| Simpl (f, o) ->
+ let () =
+ if not (simplIsCbn () || List.is_empty f.rConst) then
+ warn_simpl_unfolding_modifiers () in
+ let f = if simplIsCbn () then make_flag env f else CClosure.all (* dummy *) in
+ Simpl (f, o)
+| Cbv f -> Cbv (make_flag env f)
+| Cbn f -> Cbn (make_flag env f)
+| Lazy f -> Lazy (make_flag env f)
+| ExtraRedExpr s ->
+ begin match String.Map.find s !red_expr_tab with
+ | e -> eval_red_expr env e
+ | exception Not_found -> ExtraRedExpr s (* delay to runtime interpretation *)
+ end
+| (Red _ | Hnf | Unfold _ | Fold _ | Pattern _ | CbvVm _ | CbvNative _) as e -> e
+
+let reduction_of_red_expr_val = function
| Red internal ->
if internal then (e_red try_red_product,DEFAULTcast)
else (e_red red_product,DEFAULTcast)
| Hnf -> (e_red hnf_constr,DEFAULTcast)
| Simpl (f,o) ->
- let whd_am = if simplIsCbn () then whd_cbn (make_flag f) else whd_simpl in
- let am = if simplIsCbn () then strong_cbn (make_flag f) else simpl in
- let () =
- if not (simplIsCbn () || List.is_empty f.rConst) then
- warn_simpl_unfolding_modifiers () in
+ let whd_am = if simplIsCbn () then whd_cbn f else whd_simpl in
+ let am = if simplIsCbn () then strong_cbn f else simpl in
(contextualize (if head_style then whd_am else am) am o,DEFAULTcast)
- | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)
+ | Cbv f -> (e_red (cbv_norm_flags f),DEFAULTcast)
| Cbn f ->
- (e_red (strong_cbn (make_flag f)), DEFAULTcast)
- | Lazy f -> (e_red (clos_norm_flags (make_flag f)),DEFAULTcast)
+ (e_red (strong_cbn f), DEFAULTcast)
+ | Lazy f -> (e_red (clos_norm_flags f),DEFAULTcast)
| Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast)
| Fold cl -> (e_red (fold_commands cl),DEFAULTcast)
| Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast)
| ExtraRedExpr s ->
(try (e_red (String.Map.find s !reduction_tab),DEFAULTcast)
with Not_found ->
- (try reduction_of_red_expr (String.Map.find s !red_expr_tab)
- with Not_found ->
user_err ~hdr:"Redexpr.reduction_of_red_expr"
- (str "unknown user-defined reduction \"" ++ str s ++ str "\"")))
+ (str "unknown user-defined reduction \"" ++ str s ++ str "\""))
| CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
| CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast)
+
+let reduction_of_red_expr env r =
+ reduction_of_red_expr_val (eval_red_expr env r)
+
+(* Possibly equip a reduction with the occurrences mentioned in an
+ occurrence clause *)
+
+let error_illegal_clause () =
+ CErrors.user_err Pp.(str "\"at\" clause not supported in presence of an occurrence clause.")
+
+let error_illegal_non_atomic_clause () =
+ CErrors.user_err Pp.(str "\"at\" clause not supported in presence of a non atomic \"in\" clause.")
+
+let error_occurrences_not_unsupported () =
+ CErrors.user_err Pp.(str "Occurrences not supported for this reduction tactic.")
+
+let bind_red_expr_occurrences occs nbcl redexp =
+ let open Locus in
+ let has_at_clause = function
+ | Unfold l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
+ | Pattern l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
+ | Simpl (_,Some (occl,_)) -> occl != AllOccurrences
+ | _ -> false in
+ if occs == AllOccurrences then
+ if nbcl > 1 && has_at_clause redexp then
+ error_illegal_non_atomic_clause ()
+ else
+ redexp
+ else
+ match redexp with
+ | Unfold (_::_::_) ->
+ error_illegal_clause ()
+ | Unfold [(occl,c)] ->
+ if occl != AllOccurrences then
+ error_illegal_clause ()
+ else
+ Unfold [(occs,c)]
+ | Pattern (_::_::_) ->
+ error_illegal_clause ()
+ | Pattern [(occl,c)] ->
+ if occl != AllOccurrences then
+ error_illegal_clause ()
+ else
+ Pattern [(occs,c)]
+ | Simpl (f,Some (occl,c)) ->
+ if occl != AllOccurrences then
+ error_illegal_clause ()
+ else
+ Simpl (f,Some (occs,c))
+ | CbvVm (Some (occl,c)) ->
+ if occl != AllOccurrences then
+ error_illegal_clause ()
+ else
+ CbvVm (Some (occs,c))
+ | CbvNative (Some (occl,c)) ->
+ if occl != AllOccurrences then
+ error_illegal_clause ()
+ else
+ CbvNative (Some (occs,c))
+ | Red _ | Hnf | Cbv _ | Lazy _ | Cbn _
+ | ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None ->
+ error_occurrences_not_unsupported ()
+ | Unfold [] | Pattern [] ->
+ assert false
+
+let reduction_of_red_expr_val ?occs r =
+ let r = match occs with
+ | None -> r
+ | Some (occs, nbcl) -> bind_red_expr_occurrences occs nbcl r
in
- reduction_of_red_expr
+ reduction_of_red_expr_val r
let subst_mps subst c =
EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
diff --git a/tactics/redexpr.mli b/tactics/redexpr.mli
index d43785218f..5f3a7b689b 100644
--- a/tactics/redexpr.mli
+++ b/tactics/redexpr.mli
@@ -19,10 +19,18 @@ open Reductionops
open Locus
type red_expr =
- (constr, evaluable_global_reference, constr_pattern) red_expr_gen
+ (constr, evaluable_global_reference, constr_pattern) red_expr_gen
+
+type red_expr_val
val out_with_occurrences : 'a with_occurrences -> occurrences * 'a
+val eval_red_expr : Environ.env -> red_expr -> red_expr_val
+
+val reduction_of_red_expr_val : ?occs:(Locus.occurrences_expr * int) ->
+ red_expr_val -> e_reduction_function * cast_kind
+
+(** Composition of {!reduction_of_red_expr_val} with {!eval_red_expr} *)
val reduction_of_red_expr :
Environ.env -> red_expr -> e_reduction_function * cast_kind
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 24aa178ed2..68afd9a128 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -727,6 +727,32 @@ module New = struct
let (loc,_) = evi.Evd.evar_source in
Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None
+ let tclMAPDELAYEDWITHHOLES accept_unresolved_holes l tac =
+ let rec aux = function
+ | [] -> tclUNIT ()
+ | x :: l ->
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma_initial = Proofview.Goal.sigma gl in
+ let (sigma, x) = x env sigma_initial in
+ Proofview.Unsafe.tclEVARS sigma <*> tac x >>= fun () -> aux l >>= fun () ->
+ if accept_unresolved_holes then
+ tclUNIT ()
+ else
+ tclEVARMAP >>= fun sigma_final ->
+ try
+ let () = check_evars env sigma_final sigma sigma_initial in
+ tclUNIT ()
+ with e when CErrors.noncritical e ->
+ let e, info = Exninfo.capture e in
+ tclZERO ~info e
+ end in
+ aux l
+
+ (* The following is basically
+ tclMAPDELAYEDWITHHOLES accept_unresolved_holes [fun _ _ -> (sigma,())] (fun () -> tac)
+ but with value not necessarily in unit *)
+
let tclWITHHOLES accept_unresolved_holes tac sigma =
tclEVARMAP >>= fun sigma_initial ->
if sigma == sigma_initial then tac
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index e97c5f3c1f..19d08dcc36 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -209,6 +209,10 @@ module New : sig
val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic
val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic
+ val tclMAPDELAYEDWITHHOLES : bool -> 'a delayed_open list -> ('a -> unit tactic) -> unit tactic
+ (* in [tclMAPDELAYEDWITHHOLES with_evars l tac] the delayed
+ argument of [l] are evaluated in the possibly-updated
+ environment and updated sigma of each new successive goals *)
val tclTIMEOUT : int -> unit tactic -> unit tactic
val tclTIME : string option -> 'a tactic -> 'a tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e3369bc9be..39c5c9562f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -85,24 +85,6 @@ let () =
optread = (fun () -> !universal_lemma_under_conjunctions) ;
optwrite = (fun b -> universal_lemma_under_conjunctions := b) }
-(* The following boolean governs what "intros []" do on examples such
- as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]";
- if false, it behaves as "intro H; case H; clear H" for fresh H.
- Kept as false for compatibility.
- *)
-
-let bracketing_last_or_and_intro_pattern = ref true
-
-let use_bracketing_last_or_and_intro_pattern () =
- !bracketing_last_or_and_intro_pattern
-
-let () =
- declare_bool_option
- { optdepr = true;
- optkey = ["Bracketing";"Last";"Introduction";"Pattern"];
- optread = (fun () -> !bracketing_last_or_and_intro_pattern);
- optwrite = (fun b -> bracketing_last_or_and_intro_pattern := b) }
-
(*********************************************)
(* Tactics *)
(*********************************************)
@@ -634,70 +616,10 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where env sigma dec
in
(sigma, LocalDef (id,b',ty'))
-(* Possibly equip a reduction with the occurrences mentioned in an
- occurrence clause *)
-
-let error_illegal_clause () =
- error "\"at\" clause not supported in presence of an occurrence clause."
-
-let error_illegal_non_atomic_clause () =
- error "\"at\" clause not supported in presence of a non atomic \"in\" clause."
-
-let error_occurrences_not_unsupported () =
- error "Occurrences not supported for this reduction tactic."
-
let bind_change_occurrences occs = function
| None -> None
| Some c -> Some (Redexpr.out_with_occurrences (occs,c))
-let bind_red_expr_occurrences occs nbcl redexp =
- let has_at_clause = function
- | Unfold l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
- | Pattern l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
- | Simpl (_,Some (occl,_)) -> occl != AllOccurrences
- | _ -> false in
- if occs == AllOccurrences then
- if nbcl > 1 && has_at_clause redexp then
- error_illegal_non_atomic_clause ()
- else
- redexp
- else
- match redexp with
- | Unfold (_::_::_) ->
- error_illegal_clause ()
- | Unfold [(occl,c)] ->
- if occl != AllOccurrences then
- error_illegal_clause ()
- else
- Unfold [(occs,c)]
- | Pattern (_::_::_) ->
- error_illegal_clause ()
- | Pattern [(occl,c)] ->
- if occl != AllOccurrences then
- error_illegal_clause ()
- else
- Pattern [(occs,c)]
- | Simpl (f,Some (occl,c)) ->
- if occl != AllOccurrences then
- error_illegal_clause ()
- else
- Simpl (f,Some (occs,c))
- | CbvVm (Some (occl,c)) ->
- if occl != AllOccurrences then
- error_illegal_clause ()
- else
- CbvVm (Some (occs,c))
- | CbvNative (Some (occl,c)) ->
- if occl != AllOccurrences then
- error_illegal_clause ()
- else
- CbvNative (Some (occs,c))
- | Red _ | Hnf | Cbv _ | Lazy _ | Cbn _
- | ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None ->
- error_occurrences_not_unsupported ()
- | Unfold [] | Pattern [] ->
- assert false
-
(* The following two tactics apply an arbitrary
reduction function either to the conclusion or to a
certain hypothesis *)
@@ -959,17 +881,16 @@ let reduce redexp cl =
| Red _ | Hnf | CbvVm _ | CbvNative _ -> StableHypConv
| ExtraRedExpr _ -> StableHypConv (* Should we be that lenient ?*)
in
+ let redexp = Redexpr.eval_red_expr env redexp in
begin match cl.concl_occs with
| NoOccurrences -> Proofview.tclUNIT ()
| occs ->
- let redexp = bind_red_expr_occurrences occs nbcl redexp in
- let redfun = Redexpr.reduction_of_red_expr env redexp in
+ let redfun = Redexpr.reduction_of_red_expr_val ~occs:(occs, nbcl) redexp in
e_change_in_concl ~check (revert_cast redfun)
end
<*>
let f (id, occs, where) =
- let redexp = bind_red_expr_occurrences occs nbcl redexp in
- let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in
+ let (redfun, _) = Redexpr.reduction_of_red_expr_val ~occs:(occs, nbcl) redexp in
let redfun _ env sigma c = redfun env sigma c in
let redfun env sigma d = e_pf_change_decl redfun where env sigma d in
(id, redfun)
@@ -1083,10 +1004,10 @@ let intros_using_then l tac = intros_using_then_helper tac [] l
let intros = Tacticals.New.tclREPEAT intro
-let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
+let intro_forthcoming_then_gen name_flag move_flag dep_flag bound n tac =
let rec aux n ids =
(* Note: we always use the bound when there is one for "*" and "**" *)
- if (match bound with None -> true | Some (_,p) -> n < p) then
+ if (match bound with None -> true | Some p -> n < p) then
Proofview.tclORELSE
begin
intro_then_gen name_flag move_flag false dep_flag
@@ -1380,20 +1301,18 @@ let do_replace id = function
let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac =
let clenv = Clenv.clenv_pose_dependent_evars ~with_evars clenv in
- let clenv =
- { clenv with evd = Typeclasses.resolve_typeclasses
- ~fail:(not with_evars) clenv.env clenv.evd }
- in
+ let evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd in
+ let clenv = Clenv.update_clenv_evd clenv evd in
let new_hyp_typ = clenv_type clenv in
if not with_evars then check_unresolved_evars_of_metas sigma0 clenv;
- if not with_evars && occur_meta clenv.evd new_hyp_typ then
+ if not with_evars && occur_meta evd new_hyp_typ then
error_uninstantiated_metas new_hyp_typ clenv;
let new_hyp_prf = clenv_value clenv in
let exact_tac = Logic.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in
let naming = NamingMustBe (CAst.make targetid) in
let with_clear = do_replace (Some id) naming in
Tacticals.New.tclTHEN
- (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd))
+ (Proofview.Unsafe.tclEVARS (clear_metas evd))
(Tacticals.New.tclTHENLAST
(assert_after_then_gen ?err with_clear naming new_hyp_typ tac) exact_tac)
@@ -2282,10 +2201,9 @@ let left_with_bindings with_evars = constructor_tac with_evars (Some 2) 1
let right_with_bindings with_evars = constructor_tac with_evars (Some 2) 2
let split_with_bindings with_evars l =
Tacticals.New.tclMAP (constructor_tac with_evars (Some 1) 1) l
-let split_with_delayed_bindings with_evars =
- Tacticals.New.tclMAP (fun bl ->
- Tacticals.New.tclDELAYEDWITHHOLES with_evars bl
- (constructor_tac with_evars (Some 1) 1))
+let split_with_delayed_bindings with_evars bl =
+ Tacticals.New.tclMAPDELAYEDWITHHOLES with_evars bl
+ (constructor_tac with_evars (Some 1) 1)
let left = left_with_bindings false
let simplest_left = left NoBindings
@@ -2307,7 +2225,7 @@ let (forward_general_rewrite_clause, general_rewrite_clause) = Hook.make ()
let (forward_subst_one, subst_one) = Hook.make ()
let error_unexpected_extra_pattern loc bound pat =
- let _,nb = Option.get bound in
+ let nb = Option.get bound in
let s1,s2,s3 = match pat with
| IntroNaming (IntroIdentifier _) ->
"name", (String.plural nb " introduction pattern"), "no"
@@ -2340,14 +2258,14 @@ let intro_decomp_eq ?loc l thin tac id =
match my_find_eq_data_decompose env sigma t with
| Some (eq,u,eq_args) ->
!intro_decomp_eq_function
- (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l)
+ (fun n -> tac ((CAst.make id)::thin) (Some n) l)
(eq,t,eq_args) (c, t)
| None ->
let info = Exninfo.reify () in
Tacticals.New.tclZEROMSG ~info (str "Not a primitive equality here.")
end
-let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id =
+let intro_or_and_pattern ?loc with_evars ll thin tac id =
Proofview.Goal.enter begin fun gl ->
let c = mkVar id in
let env = Proofview.Goal.env gl in
@@ -2361,11 +2279,11 @@ let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id =
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Tacticals.New.tclTHENLASTn
(Tacticals.New.tclTHEN (simplest_ecase c) (clear [id]))
- (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
+ (Array.map2 (fun n l -> tac thin (Some n) l)
nv_with_let ll))
end
-let rewrite_hyp_then assert_style with_evars thin l2r id tac =
+let rewrite_hyp_then with_evars thin l2r id tac =
let rew_on l2r =
Hook.get forward_general_rewrite_clause l2r with_evars (mkVar id,NoBindings) in
let subst_on l2r x rhs =
@@ -2477,11 +2395,11 @@ let make_tmp_naming avoid l = function
let fit_bound n = function
| None -> true
- | Some (use_bound,n') -> not use_bound || n = n'
+ | Some n' -> n = n'
let exceed_bound n = function
| None -> false
- | Some (use_bound,n') -> use_bound && n >= n'
+ | Some n' -> n >= n'
(* We delay thinning until the completion of the whole intros tactic
to ensure that dependent hypotheses are cleared in the right
@@ -2502,60 +2420,59 @@ let exceed_bound n = function
[patl]: introduction patterns to interpret
*)
-let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac =
+let rec intro_patterns_core with_evars avoid ids thin destopt bound n tac =
function
| [] when fit_bound n bound ->
tac ids thin
| [] ->
(* Behave as IntroAnonymous *)
- intro_patterns_core with_evars b avoid ids thin destopt bound n tac
+ intro_patterns_core with_evars avoid ids thin destopt bound n tac
[CAst.make @@ IntroNaming IntroAnonymous]
| {CAst.loc;v=pat} :: l ->
if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else
match pat with
| IntroForthcoming onlydeps ->
intro_forthcoming_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l)))
- destopt onlydeps n bound
- (fun ids -> intro_patterns_core with_evars b avoid ids thin destopt bound
+ destopt onlydeps bound n
+ (fun ids -> intro_patterns_core with_evars 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 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
+ (intro_pattern_action ?loc with_evars pat thin destopt
+ (fun thin bound' -> intro_patterns_core with_evars avoid ids thin destopt bound' 0
(fun ids thin ->
- intro_patterns_core with_evars b avoid ids thin destopt bound (n+1) tac l)))
+ intro_patterns_core with_evars avoid ids thin destopt bound (n+1) tac l)))
| IntroNaming pat ->
- intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound (n+1) tac l
+ intro_pattern_naming loc with_evars avoid ids pat thin destopt bound (n+1) tac l
(* Pi-introduction rule, used backwards *)
-and intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound n tac l =
+and intro_pattern_naming loc with_evars 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 CAst.(make ?loc id)) destopt true false
- (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l))
+ (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l))
| IntroAnonymous ->
intro_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l)))
destopt true false
- (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)
+ (fun id -> intro_patterns_core with_evars 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, Id.Set.union avoid (explicit_intro_names l)))
destopt true false
- (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)
+ (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l)
-and intro_pattern_action ?loc with_evars b style pat thin destopt tac id =
+and intro_pattern_action ?loc with_evars pat thin destopt tac id =
match pat with
| IntroWildcard ->
tac (CAst.(make ?loc id)::thin) None []
| IntroOrAndPattern ll ->
- intro_or_and_pattern ?loc with_evars b ll thin tac id
+ intro_or_and_pattern ?loc with_evars ll thin tac id
| IntroInjection l' ->
intro_decomp_eq ?loc l' thin tac id
| IntroRewrite l2r ->
- rewrite_hyp_then style with_evars thin l2r id (fun thin -> tac thin None [])
+ rewrite_hyp_then with_evars thin l2r id (fun thin -> tac thin None [])
| IntroApplyOn ({CAst.loc=loc';v=f},{CAst.loc;v=pat}) ->
let naming,tac_ipat =
prepare_intros ?loc with_evars (IntroIdentifier id) destopt pat in
@@ -2576,28 +2493,26 @@ and prepare_intros ?loc with_evars dft destopt = function
| IntroAction ipat ->
prepare_naming ?loc dft,
(let tac thin bound =
- intro_patterns_core with_evars true Id.Set.empty [] thin destopt bound 0
+ intro_patterns_core with_evars Id.Set.empty [] thin destopt bound 0
(fun _ l -> clear_wildcards l) in
fun id ->
- intro_pattern_action ?loc with_evars true true ipat [] destopt tac id)
+ intro_pattern_action ?loc with_evars ipat [] destopt tac id)
| IntroForthcoming _ -> user_err ?loc
(str "Introduction pattern for one hypothesis expected.")
-let intro_patterns_head_core with_evars b destopt bound pat =
+let intro_patterns_head_core with_evars destopt bound pat =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
check_name_unicity env [] [] pat;
- intro_patterns_core with_evars b Id.Set.empty [] [] destopt
+ intro_patterns_core with_evars Id.Set.empty [] [] destopt
bound 0 (fun _ l -> clear_wildcards l) pat
end
let intro_patterns_bound_to with_evars n destopt =
- intro_patterns_head_core with_evars true destopt
- (Some (true,n))
+ intro_patterns_head_core with_evars destopt (Some n)
let intro_patterns_to with_evars destopt =
- intro_patterns_head_core with_evars (use_bracketing_last_or_and_intro_pattern ())
- destopt None
+ intro_patterns_head_core with_evars destopt None
let intro_pattern_to with_evars destopt pat =
intro_patterns_to with_evars destopt [CAst.make pat]
@@ -2635,7 +2550,7 @@ let assert_as first hd ipat t =
(* apply in as *)
let general_apply_in ?(respect_opaque=false) with_delta
- with_destruct with_evars id lemmas ipat =
+ with_destruct with_evars id lemmas ipat then_tac =
let tac (naming,lemma) tac id =
apply_in_delayed_once ~respect_opaque with_delta
with_destruct with_evars naming id lemma tac in
@@ -2653,7 +2568,8 @@ let general_apply_in ?(respect_opaque=false) with_delta
List.map (fun lem -> (NamingMustBe (CAst.make id),lem)) first, (naming,last)
in
(* We chain apply_in_once, ending with an intro pattern *)
- List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id
+ List.fold_right tac lemmas_target
+ (tac last_lemma_target (fun id -> Tacticals.New.tclTHEN (ipat_tac id) then_tac)) id
end
(*
@@ -2666,10 +2582,10 @@ let general_apply_in ?(respect_opaque=false) with_delta
let apply_in simple with_evars id lemmas ipat =
let lemmas = List.map (fun (k,{CAst.loc;v=l}) -> k, CAst.make ?loc (fun _ sigma -> (sigma,l))) lemmas in
- general_apply_in simple simple with_evars id lemmas ipat
+ general_apply_in simple simple with_evars id lemmas ipat Tacticals.New.tclIDTAC
-let apply_delayed_in simple with_evars id lemmas ipat =
- general_apply_in ~respect_opaque:true simple simple with_evars id lemmas ipat
+let apply_delayed_in simple with_evars id lemmas ipat then_tac =
+ general_apply_in ~respect_opaque:true simple simple with_evars id lemmas ipat then_tac
(*****************************)
(* Tactics abstracting terms *)
@@ -3271,7 +3187,7 @@ let re_intro_dependent_hypotheses (lstatus,rstatus) (_,tophyp) =
(intros_move newlstatus)
let dest_intro_patterns with_evars avoid thin dest pat tac =
- intro_patterns_core with_evars true avoid [] thin dest None 0 tac pat
+ intro_patterns_core with_evars avoid [] thin dest None 0 tac pat
let safe_dest_intro_patterns with_evars avoid thin dest pat tac =
Proofview.tclORELSE
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 54c781af5c..0fd2f1253f 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -233,7 +233,7 @@ val apply_in :
val apply_delayed_in :
advanced_flag -> evars_flag -> Id.t ->
(clear_flag * delayed_open_constr_with_bindings CAst.t) list ->
- intro_pattern option -> unit Proofview.tactic
+ intro_pattern option -> unit Proofview.tactic -> unit Proofview.tactic
(** {6 Elimination tactics. } *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 11:15:24 +0000