aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml18
-rw-r--r--tactics/autorewrite.ml7
-rw-r--r--tactics/class_tactics.ml49
-rw-r--r--tactics/contradiction.ml17
-rw-r--r--tactics/eauto.ml6
-rw-r--r--tactics/elim.ml3
-rw-r--r--tactics/eqdecide.ml4
-rw-r--r--tactics/eqschemes.ml2
-rw-r--r--tactics/equality.ml131
-rw-r--r--tactics/hints.ml4
-rw-r--r--tactics/hipattern.ml8
-rw-r--r--tactics/tacticals.ml50
-rw-r--r--tactics/tacticals.mli4
-rw-r--r--tactics/tactics.ml169
-rw-r--r--tactics/tactics.mli6
15 files changed, 336 insertions, 142 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 5b06088518..681c4e910f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -137,8 +137,9 @@ let conclPattern concl pat tac =
| Some pat ->
try
Proofview.tclUNIT (Constr_matching.matches env sigma pat concl)
- with Constr_matching.PatternMatchingFailure ->
- Tacticals.New.tclZEROMSG (str "pattern-matching failed")
+ with Constr_matching.PatternMatchingFailure as exn ->
+ let _, info = Exninfo.capture exn in
+ Tacticals.New.tclZEROMSG ~info (str "pattern-matching failed")
in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -383,7 +384,9 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
let tactic = function
| Res_pf (c,cl) -> unify_resolve_gen ~poly flags (c,cl)
- | ERes_pf _ -> Proofview.Goal.enter (fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf"))
+ | ERes_pf _ -> Proofview.Goal.enter (fun gl ->
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (str "eres_pf"))
| Give_exact (c, cl) -> exact poly (c, cl)
| Res_pf_THEN_trivial_fail (c,cl) ->
Tacticals.New.tclTHEN
@@ -395,7 +398,9 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
Proofview.Goal.enter begin fun gl ->
if exists_evaluable_reference (Tacmach.New.pf_env gl) c then
Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)
- else Tacticals.New.tclFAIL 0 (str"Unbound reference")
+ else
+ let info = Exninfo.reify () in
+ Tacticals.New.tclFAIL ~info 0 (str"Unbound reference")
end
| Extern tacast ->
conclPattern concl p tacast
@@ -492,7 +497,10 @@ let search d n mod_delta db_list local_db =
(* spiwack: the test of [n] to 0 must be done independently in
each goal. Hence the [tclEXTEND] *)
Proofview.tclEXTEND [] begin
- if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else
+ if Int.equal n 0 then
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (str"BOUND 2")
+ else
Tacticals.New.tclORELSE0 (dbg_assumption d)
(Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
( Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index ac83acd726..eaefa2947a 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -154,7 +154,8 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
if not (Locusops.is_all_occurrences cl.concl_occs) &&
cl.concl_occs != NoOccurrences
then
- Tacticals.New.tclZEROMSG (str"The \"at\" syntax isn't available yet for the autorewrite tactic.")
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (str"The \"at\" syntax isn't available yet for the autorewrite tactic.")
else
let compose_tac t1 t2 =
match cl.onhyps with
@@ -185,7 +186,9 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl =
*)
Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds tac_main lbas cl)
| _ ->
- Tacticals.New.tclZEROMSG (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info
+ (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")
(* Functions necessary to the library object declaration *)
let cache_hintrewrite (_,(rbase,lrl)) =
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index a51fc8b347..80c76bee60 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -166,7 +166,9 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' =
Proofview.Goal.enter begin fun gls ->
let resolve =
try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls)
- with e when noncritical e -> Proofview.tclZERO e
+ with e when noncritical e ->
+ let _, info = Exninfo.capture e in
+ Proofview.tclZERO ~info e
in resolve >>= fun clenv' ->
Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv'
end
@@ -207,12 +209,14 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
let unify_resolve_refine poly flags gl clenv =
Proofview.tclORELSE
(unify_resolve_refine poly flags gl clenv)
- (fun ie ->
- match fst ie with
+ (fun (exn,info) ->
+ match exn with
| Evarconv.UnableToUnify _ ->
- Tacticals.New.tclZEROMSG (str "Unable to unify")
- | e ->
- Tacticals.New.tclZEROMSG (str "Unexpected error"))
+ Tacticals.New.tclZEROMSG ~info (str "Unable to unify")
+ | e when CErrors.noncritical e ->
+ Tacticals.New.tclZEROMSG ~info (str "Unexpected error")
+ | _ ->
+ Exninfo.iraise (exn,info))
(** Dealing with goals of the form A -> B and hints of the form
C -> A -> B.
@@ -234,10 +238,13 @@ let with_prods nprods poly (c, clenv) f =
if get_typeclasses_limit_intros () then
Proofview.Goal.enter begin fun gl ->
try match clenv_of_prods poly nprods (c, clenv) gl with
- | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
+ | None ->
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (str"Not enough premisses")
| Some (diff, clenv') -> f gl (c, diff, clenv')
with e when CErrors.noncritical e ->
- Tacticals.New.tclZEROMSG (CErrors.print e) end
+ let e, info = Exninfo.capture e in
+ Tacticals.New.tclZEROMSG ~info (CErrors.print e) end
else Proofview.Goal.enter
begin fun gl ->
if Int.equal nprods 0 then f gl (c, None, clenv)
@@ -811,7 +818,9 @@ module Search = struct
search_tac hints limit (succ depth) info
in
fun info ->
- if Int.equal depth (succ limit) then Proofview.tclZERO ReachedLimitEx
+ if Int.equal depth (succ limit) then
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info ReachedLimitEx
else
Proofview.tclOR (hints_tac hints info kont)
(fun e -> Proofview.tclOR (intro info kont)
@@ -860,9 +869,13 @@ module Search = struct
let fix_iterative_limit limit t =
let open Proofview in
let rec aux depth =
- if Int.equal depth (succ limit) then tclZERO ReachedLimitEx
- else tclOR (t depth) (function (ReachedLimitEx, _) -> aux (succ depth)
- | (e,ie) -> Proofview.tclZERO ~info:ie e)
+ if Int.equal depth (succ limit)
+ then
+ let info = Exninfo.reify () in
+ tclZERO ~info ReachedLimitEx
+ else tclOR (t depth) (function
+ | (ReachedLimitEx, _) -> aux (succ depth)
+ | (e,ie) -> Proofview.tclZERO ~info:ie e)
in aux 1
let eauto_tac_stuck mst ?(unique=false)
@@ -884,18 +897,18 @@ module Search = struct
| None -> fix_iterative search
| Some l -> fix_iterative_limit l search
in
- let error (e, ie) =
+ let error (e, info) =
match e with
| ReachedLimitEx ->
- Tacticals.New.tclFAIL 0 (str"Proof search reached its limit")
+ Tacticals.New.tclFAIL ~info 0 (str"Proof search reached its limit")
| NoApplicableEx ->
- Tacticals.New.tclFAIL 0 (str"Proof search failed" ++
+ Tacticals.New.tclFAIL ~info 0 (str"Proof search failed" ++
(if Option.is_empty depth then mt()
else str" without reaching its limit"))
| Proofview.MoreThanOneSuccess ->
- Tacticals.New.tclFAIL 0 (str"Proof search failed: " ++
- str"more than one success found")
- | e -> Proofview.tclZERO ~info:ie e
+ Tacticals.New.tclFAIL ~info 0 (str"Proof search failed: " ++
+ str"more than one success found")
+ | e -> Proofview.tclZERO ~info e
in
let tac = Proofview.tclOR tac error in
let tac =
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index d6be714dd9..8ad3d072ec 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -49,7 +49,9 @@ let absurd c = absurd c
(** [f] does not assume its argument to be [nf_evar]-ed. *)
let filter_hyp f tac =
let rec seek = function
- | [] -> Proofview.tclZERO Not_found
+ | [] ->
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info Not_found
| d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d)
| _::rest -> seek rest in
Proofview.Goal.enter begin fun gl ->
@@ -62,7 +64,9 @@ let contradiction_context =
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let rec seek_neg l = match l with
- | [] -> Tacticals.New.tclZEROMSG (Pp.str"No such contradiction")
+ | [] ->
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (Pp.str"No such contradiction")
| d :: rest ->
let id = NamedDecl.get_id d in
let typ = nf_evar sigma (NamedDecl.get_type d) in
@@ -83,7 +87,8 @@ let contradiction_context =
(* Checking on the fly that it type-checks *)
simplest_elim (mkApp (mkVar id,[|p|]))
| None ->
- Tacticals.New.tclZEROMSG (Pp.str"Not a negated unit type."))
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (Pp.str"Not a negated unit type."))
(Proofview.tclORELSE
(Proofview.Goal.enter begin fun gl ->
let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in
@@ -123,10 +128,12 @@ let contradiction_term (c,lbind as cl) =
filter_hyp (fun c -> is_negation_of env sigma typ c)
(fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
else
- Proofview.tclZERO Not_found
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info Not_found
end
begin function (e, info) -> match e with
- | Not_found -> Tacticals.New.tclZEROMSG (Pp.str"Not a contradiction.")
+ | Not_found ->
+ Tacticals.New.tclZEROMSG ~info (Pp.str"Not a contradiction.")
| e -> Proofview.tclZERO ~info e
end
end
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 28b5ed5811..710e0a6808 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -485,7 +485,7 @@ let unfold_head env sigma (ids, csts) c =
true, EConstr.of_constr (Environ.constant_value_in env (cst, u))
| App (f, args) ->
(match aux f with
- | true, f' -> true, Reductionops.whd_betaiota sigma (mkApp (f', args))
+ | true, f' -> true, Reductionops.whd_betaiota env sigma (mkApp (f', args))
| false, _ ->
let done_, args' =
Array.fold_left_i (fun i (done_, acc) arg ->
@@ -526,5 +526,7 @@ let autounfold_one db cl =
match cl with
| Some hyp -> change_in_hyp ~check:true None (make_change_arg c') hyp
| None -> convert_concl ~check:false c' DEFAULTcast
- else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
+ else
+ let info = Exninfo.reify () in
+ Tacticals.New.tclFAIL ~info 0 (str "Nothing to unfold")
end
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 5d8698916f..415c980c2a 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -160,7 +160,8 @@ let double_ind h1 h2 =
let abs =
if abs_i < abs_j then Proofview.tclUNIT (abs_i,abs_j) else
if abs_i > abs_j then Proofview.tclUNIT (abs_j,abs_i) else
- tclZEROMSG (Pp.str "Both hypotheses are the same.") in
+ let info = Exninfo.reify () in
+ tclZEROMSG ~info (Pp.str "Both hypotheses are the same.") in
abs >>= fun (abs_i,abs_j) ->
(tclTHEN (tclDO abs_i intro)
(onLastHypId
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 6fbd29def9..57d793b2a5 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -182,7 +182,9 @@ let match_eqdec env sigma c =
let neq = mkApp (noteq,[|mkApp (eq2,[|t;x;y|])|]) in
if eqonleft then mkApp (op,[|eq;neq|]) else mkApp (op,[|neq;eq|]) in
Proofview.tclUNIT (eqonleft,mk,c1,c2,ty)
- with PatternMatchingFailure -> Proofview.tclZERO PatternMatchingFailure
+ with PatternMatchingFailure as exn ->
+ let _, info = Exninfo.capture exn in
+ Proofview.tclZERO ~info PatternMatchingFailure
(* /spiwack *)
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 7c702eab3a..6da2248cc3 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -653,7 +653,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
(mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p)
(mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp)
(mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind)
- (EConstr.Unsafe.to_constr (Reductionops.whd_beta sigma
+ (EConstr.Unsafe.to_constr (Reductionops.whd_beta env sigma
(EConstr.of_constr (applist (c,
Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))))
in c', ctx'
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e1d34af13e..79b6dfe920 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -280,8 +280,9 @@ let general_elim_clause with_evars frzevars cls rew elim =
end
begin function (e, info) -> match e with
| PretypeError (env, evd, NoOccurrenceFound (c', _)) ->
- Proofview.tclZERO (PretypeError (env, evd, NoOccurrenceFound (c', cls)))
- | e -> Proofview.tclZERO ~info e
+ Proofview.tclZERO ~info (PretypeError (env, evd, NoOccurrenceFound (c', cls)))
+ | e ->
+ Proofview.tclZERO ~info e
end
let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
@@ -423,7 +424,8 @@ let type_of_clause cls gl = match cls with
let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
Proofview.Goal.enter begin fun gl ->
let evd = Proofview.Goal.sigma gl in
- let isatomic = isProd evd (whd_zeta evd hdcncl) in
+ let env = Proofview.Goal.env gl in
+ let isatomic = isProd evd (whd_zeta env evd hdcncl) in
let dep_fun = if isatomic then dependent else dependent_no_evar in
let type_of_cls = type_of_clause cls gl in
let dep = dep_proof_ok && dep_fun evd c type_of_cls in
@@ -458,7 +460,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let ctype = get_type_of env sigma c in
- let rels, t = decompose_prod_assum sigma (whd_betaiotazeta sigma ctype) in
+ let rels, t = decompose_prod_assum sigma (whd_betaiotazeta env sigma ctype) in
match match_with_equality_type env sigma t with
| Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
let lft2rgt = adjust_rewriting_direction args lft2rgt in
@@ -475,7 +477,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
Proofview.tclEVARMAP >>= fun sigma ->
let env' = push_rel_context rels env in
let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
- match match_with_equality_type env sigma t' with
+ match match_with_equality_type env' sigma t' with
| Some (hdcncl,args) ->
let lft2rgt = adjust_rewriting_direction args lft2rgt in
leibniz_rewrite_ebindings_clause cls lft2rgt tac c
@@ -1035,7 +1037,9 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
Proofview.tclUNIT
(build_discriminator e_env sigma true_0 (false_0,false_ty) dirn (mkVar e) cpath)
with
- UserError _ as ex -> Proofview.tclZERO ex
+ UserError _ as ex ->
+ let _, info = Exninfo.capture ex in
+ Proofview.tclZERO ~info ex
in
discriminator >>= fun discriminator ->
discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf ->
@@ -1051,9 +1055,10 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let env = Proofview.Goal.env gl in
match find_positions env sigma ~keep_proofs:false ~no_discr:false t1 t2 with
| Inr _ ->
- tclZEROMSG (str"Not a discriminable equality.")
+ let info = Exninfo.reify () in
+ tclZEROMSG ~info (str"Not a discriminable equality.")
| Inl (cpath, (_,dirn), _) ->
- discr_positions env sigma u eq_clause cpath dirn
+ discr_positions env sigma u eq_clause cpath dirn
end
let onEquality with_evars tac (c,lbindc) =
@@ -1082,7 +1087,8 @@ let onNegatedEquality with_evars tac =
(onLastHypId (fun id ->
onEquality with_evars tac (mkVar id,NoBindings)))
| _ ->
- tclZEROMSG (str "Not a negated primitive equality.")
+ let info = Exninfo.reify () in
+ tclZEROMSG ~info (str "Not a negated primitive equality.")
end
let discrSimpleClause with_evars = function
@@ -1214,7 +1220,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
with Evarconv.UnableToUnify _ ->
user_err Pp.(str "Cannot solve a unification problem.")
else
- let (a,p_i_minus_1) = match whd_beta_stack sigma p_i with
+ let (a,p_i_minus_1) = match whd_beta_stack env sigma p_i with
| (_sigS,[a;p]) -> (a, p)
| _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in
let sigma, ev = Evarutil.new_evar env sigma a in
@@ -1624,10 +1630,11 @@ let cutSubstInHyp l2r eqn id =
let try_rewrite tac =
Proofview.tclORELSE tac begin function (e, info) -> match e with
| Constr_matching.PatternMatchingFailure ->
- tclZEROMSG (str "Not a primitive equality here.")
+ tclZEROMSG ~info (str "Not a primitive equality here.")
| e ->
- tclZEROMSG
- (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
+ (* XXX: absorbing anomalies?? *)
+ tclZEROMSG ~info
+ (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
end
let cutSubstClause l2r eqn cls =
@@ -1707,12 +1714,42 @@ let is_eq_x gl x d =
with Constr_matching.PatternMatchingFailure ->
()
+exception FoundDepInGlobal of Id.t option * GlobRef.t
+
+let test_non_indirectly_dependent_section_variable gl x =
+ let env = Proofview.Goal.env gl in
+ let sigma = Tacmach.New.project gl in
+ let hyps = Proofview.Goal.hyps gl in
+ let concl = Proofview.Goal.concl gl in
+ List.iter (fun decl ->
+ NamedDecl.iter_constr (fun c ->
+ match occur_var_indirectly env sigma x c with
+ | Some gr -> raise (FoundDepInGlobal (Some (NamedDecl.get_id decl), gr))
+ | None -> ()) decl) hyps;
+ match occur_var_indirectly env sigma x concl with
+ | Some gr -> raise (FoundDepInGlobal (None, gr))
+ | None -> ()
+
+let check_non_indirectly_dependent_section_variable gl x =
+ try test_non_indirectly_dependent_section_variable gl x
+ with FoundDepInGlobal (pos,gr) ->
+ let where = match pos with
+ | Some id -> str "hypothesis " ++ Id.print id
+ | None -> str "the conclusion of the goal" in
+ user_err ~hdr:"Subst"
+ (strbrk "Section variable " ++ Id.print x ++
+ strbrk " occurs implicitly in global declaration " ++ Printer.pr_global gr ++
+ strbrk " present in " ++ where ++ strbrk ".")
+
+let is_non_indirectly_dependent_section_variable gl z =
+ try test_non_indirectly_dependent_section_variable gl z; true
+ with FoundDepInGlobal (pos,gr) -> false
+
(* Rewrite "hyp:x=rhs" or "hyp:rhs=x" (if dir=false) everywhere and
erase hyp and x; proceed by generalizing all dep hyps *)
let subst_one dep_proof_ok x (hyp,rhs,dir) =
Proofview.Goal.enter begin fun gl ->
- let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let hyps = Proofview.Goal.hyps gl in
let concl = Proofview.Goal.concl gl in
@@ -1721,7 +1758,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) ->
let id = NamedDecl.get_id dcl in
if not (Id.equal id hyp)
- && List.exists (fun y -> occur_var_in_decl env sigma y dcl) deps
+ && List.exists (fun y -> local_occur_var_in_decl sigma y dcl) deps
then
let id_dest = if !regular_subst_tactic then dest else MoveLast in
(dest,id::deps,(id_dest,id)::allhyps)
@@ -1730,7 +1767,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
hyps
(MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *)
(* Decides if x appears in conclusion *)
- let depconcl = occur_var env sigma x concl in
+ let depconcl = local_occur_var sigma x concl in
let need_rewrite = not (List.is_empty dephyps) || depconcl in
tclTHENLIST
((if need_rewrite then
@@ -1761,6 +1798,8 @@ let subst_one_var dep_proof_ok x =
(str "Cannot find any non-recursive equality over " ++ Id.print x ++
str".")
with FoundHyp res -> res in
+ if is_section_variable x then
+ check_non_indirectly_dependent_section_variable gl x;
subst_one dep_proof_ok x res
end
@@ -1794,53 +1833,37 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
if !regular_subst_tactic then
- (* First step: find hypotheses to treat in linear time *)
- let find_equations gl =
- let env = Proofview.Goal.env gl in
- let sigma = project gl in
- let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in
- let select_equation_name decl =
+ (* Find hypotheses to treat in linear time *)
+ let process hyp =
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = project gl in
+ let c = pf_get_hyp hyp gl |> NamedDecl.get_type in
try
- let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
+ let lbeq,u,(_,x,y) = pf_apply find_eq_data_decompose gl c in
let u = EInstance.kind sigma u in
let eq = Constr.mkRef (lbeq.eq,u) in
if flags.only_leibniz then restrict_to_eq_and_identity eq;
match EConstr.kind sigma x, EConstr.kind sigma y with
- | Var z, _ when not (is_evaluable env (EvalVarRef z)) ->
- Some (NamedDecl.get_id decl)
- | _, Var z when not (is_evaluable env (EvalVarRef z)) ->
- Some (NamedDecl.get_id decl)
+ | Var x, Var y when Id.equal x y ->
+ Proofview.tclUNIT ()
+ | Var x', _ when not (Termops.local_occur_var sigma x' y) &&
+ not (is_evaluable env (EvalVarRef x')) &&
+ is_non_indirectly_dependent_section_variable gl x' ->
+ subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
+ | _, Var y' when not (Termops.local_occur_var sigma y' x) &&
+ not (is_evaluable env (EvalVarRef y')) &&
+ is_non_indirectly_dependent_section_variable gl y' ->
+ subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
| _ ->
- None
- with Constr_matching.PatternMatchingFailure -> None
+ Proofview.tclUNIT ()
+ with Constr_matching.PatternMatchingFailure ->
+ Proofview.tclUNIT ()
+ end
in
- let hyps = Proofview.Goal.hyps gl in
- List.rev (List.map_filter select_equation_name hyps)
- in
-
- (* Second step: treat equations *)
- let process hyp =
Proofview.Goal.enter begin fun gl ->
- let sigma = project gl in
- let env = Proofview.Goal.env gl in
- let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in
- let c = pf_get_hyp hyp gl |> NamedDecl.get_type in
- let _,_,(_,x,y) = find_eq_data_decompose c in
- (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
- if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else
- match EConstr.kind sigma x, EConstr.kind sigma y with
- | Var x', _ when not (Termops.local_occur_var sigma x' y) && not (is_evaluable env (EvalVarRef x')) ->
- subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
- | _, Var y' when not (Termops.local_occur_var sigma y' x) && not (is_evaluable env (EvalVarRef y')) ->
- subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
- | _ ->
- Proofview.tclUNIT ()
+ tclMAP process (List.rev (List.map NamedDecl.get_id (Proofview.Goal.hyps gl)))
end
- in
- Proofview.Goal.enter begin fun gl ->
- let ids = find_equations gl in
- tclMAP process ids
- end
else
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 5fb519cc4f..a0670ef70d 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1570,6 +1570,8 @@ let run_hint tac k = match warn_hint () with
else Proofview.tclTHEN (log_hint tac) (k tac.obj)
| HintStrict ->
if is_imported tac then k tac.obj
- else Proofview.tclZERO (UserError (None, (str "Tactic failure.")))
+ else
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info (UserError (None, (str "Tactic failure.")))
let repr_hint h = h.obj
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 76b1c94759..5338e0eef5 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -88,9 +88,9 @@ let is_lax_conjunction = function
let prod_assum sigma t = fst (decompose_prod_assum sigma t)
(* whd_beta normalize the types of arguments in a product *)
-let rec whd_beta_prod sigma c = match EConstr.kind sigma c with
- | Prod (n,t,c) -> mkProd (n,Reductionops.whd_beta sigma t,whd_beta_prod sigma c)
- | LetIn (n,d,t,c) -> mkLetIn (n,d,t,whd_beta_prod sigma c)
+let rec whd_beta_prod env sigma c = match EConstr.kind sigma c with
+ | Prod (n,t,c) -> mkProd (n,Reductionops.whd_beta env sigma t,whd_beta_prod env sigma c)
+ | LetIn (n,d,t,c) -> mkLetIn (n,d,t,whd_beta_prod env sigma c)
| _ -> c
let match_with_one_constructor env sigma style onlybinary allow_rec t =
@@ -119,7 +119,7 @@ let match_with_one_constructor env sigma style onlybinary allow_rec t =
else
let ctx, cty = mip.mind_nf_lc.(0) in
let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
- let ctyp = whd_beta_prod sigma
+ let ctyp = whd_beta_prod env sigma
(Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) cty args) in
let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in
if not (is_lax_conjunction style) || has_nodep_prod env sigma ctyp then
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 07f9def2c8..a4d306c497 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -29,6 +29,8 @@ module NamedDecl = Context.Named.Declaration
type tactic = Proofview.V82.tac
+[@@@ocaml.warning "-3"]
+
let tclIDTAC = Refiner.tclIDTAC
let tclIDTAC_MESSAGE = Refiner.tclIDTAC_MESSAGE
let tclORELSE0 = Refiner.tclORELSE0
@@ -264,22 +266,36 @@ module New = struct
let tclTHEN t1 t2 =
t1 <*> t2
- let tclFAIL lvl msg =
- tclZERO (Refiner.FailError (lvl,lazy msg))
-
- let tclZEROMSG ?loc msg =
- let err = UserError (None, msg) in
+ let tclFAIL ?info lvl msg =
+ let info = match info with
+ (* If the backtrace points here it means the caller didn't save
+ the backtrace correctly *)
+ | None -> Exninfo.reify ()
+ | Some info -> info
+ in
+ tclZERO ~info (Refiner.FailError (lvl,lazy msg))
+
+ let tclZEROMSG ?info ?loc msg =
+ let info = match info with
+ (* If the backtrace points here it means the caller didn't save
+ the backtrace correctly *)
+ | None -> Exninfo.reify ()
+ | Some info -> info
+ in
let info = match loc with
- | None -> Exninfo.null
- | Some loc -> Loc.add_loc Exninfo.null loc
+ | None -> info
+ | Some loc -> Loc.add_loc info loc
in
+ let err = UserError (None, msg) in
tclZERO ~info err
let catch_failerror e =
try
Refiner.catch_failerror e;
tclUNIT ()
- with e when CErrors.noncritical e -> tclZERO e
+ with e when CErrors.noncritical e ->
+ let _, info = Exninfo.capture e in
+ tclZERO ~info e
(* spiwack: I chose to give the Ltac + the same semantics as
[Proofview.tclOR], however, for consistency with the or-else
@@ -439,8 +455,10 @@ module New = struct
(* Try the first tactic that does not fail in a list of tactics *)
let rec tclFIRST = function
- | [] -> tclZEROMSG (str"No applicable tactic.")
- | t::rest -> tclORELSE0 t (tclFIRST rest)
+ | [] ->
+ let info = Exninfo.reify () in
+ tclZEROMSG ~info (str"No applicable tactic.")
+ | t::rest -> tclORELSE0 t (tclFIRST rest)
let rec tclFIRST_PROGRESS_ON tac = function
| [] -> tclFAIL 0 (str "No applicable tactic")
@@ -449,7 +467,8 @@ module New = struct
let rec tclDO n t =
if n < 0 then
- tclZEROMSG (str"Wrong argument : Do needs a positive integer.")
+ let info = Exninfo.reify () in
+ tclZEROMSG ~info (str"Wrong argument : Do needs a positive integer.")
else if n = 0 then tclUNIT ()
else if n = 1 then t
else tclTHEN t (tclDO (n-1) t)
@@ -472,7 +491,8 @@ module New = struct
let tclCOMPLETE t =
t >>= fun res ->
(tclINDEPENDENT
- (tclZEROMSG (str"Proof is not complete."))
+ (let info = Exninfo.reify () in
+ tclZEROMSG ~info (str"Proof is not complete."))
) <*>
tclUNIT res
@@ -531,7 +551,8 @@ module New = struct
let () = check_evars env sigma_final sigma sigma_initial in
tclUNIT x
with e when CErrors.noncritical e ->
- tclZERO e
+ let e, info = Exninfo.capture e in
+ tclZERO ~info e
else
tclUNIT x
in
@@ -550,7 +571,8 @@ module New = struct
(Proofview.tclTIMEOUT n t)
begin function (e, info) -> match e with
| Logic_monad.Tac_Timeout as e ->
- Proofview.tclZERO (Refiner.FailError (0,lazy (CErrors.print e)))
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info (Refiner.FailError (0,lazy (CErrors.print e)))
| e -> Proofview.tclZERO ~info e
end
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 01565169ca..eebe702259 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -151,9 +151,9 @@ module New : sig
(* [tclFAIL n msg] fails with [msg] as an error message at level [n]
(meaning that it will jump over [n] error catching tacticals FROM
THIS MODULE. *)
- val tclFAIL : int -> Pp.t -> 'a tactic
+ val tclFAIL : ?info:Exninfo.info -> int -> Pp.t -> 'a tactic
- val tclZEROMSG : ?loc:Loc.t -> Pp.t -> 'a tactic
+ val tclZEROMSG : ?info:Exninfo.info -> ?loc:Loc.t -> Pp.t -> 'a tactic
(** Fail with a [User_Error] containing the given message. *)
val tclOR : unit tactic -> unit tactic -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e4809332c5..5fe87a94c5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -182,10 +182,13 @@ let convert_gen pb x y =
Proofview.Goal.enter begin fun gl ->
match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with
| Some sigma -> Proofview.Unsafe.tclEVARS sigma
- | None -> Tacticals.New.tclFAIL 0 (str "Not convertible")
- | exception _ ->
+ | None ->
+ let info = Exninfo.reify () in
+ Tacticals.New.tclFAIL ~info 0 (str "Not convertible")
+ | exception e ->
+ let _, info = Exninfo.capture e in
(* FIXME: Sometimes an anomaly is raised from conversion *)
- Tacticals.New.tclFAIL 0 (str "Not convertible")
+ Tacticals.New.tclFAIL ~info 0 (str "Not convertible")
end
let convert x y = convert_gen Reduction.CONV x y
@@ -301,7 +304,9 @@ let rename_hyp repl =
let init = Some (Id.Set.empty, Id.Set.empty) in
let dom = List.fold_left fold init repl in
match dom with
- | None -> Tacticals.New.tclZEROMSG (str "Not a one-to-one name mapping")
+ | None ->
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (str "Not a one-to-one name mapping")
| Some (src, dst) ->
Proofview.Goal.enter begin fun gl ->
let hyps = Proofview.Goal.hyps gl in
@@ -1023,7 +1028,10 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
(Proofview.Unsafe.tclEVARS sigma)
(intro_then_gen name_flag move_flag force_flag dep_flag tac)
| _ ->
- begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct))
+ begin if not force_flag
+ then
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info (RefinerError (env, sigma, IntroNeedsProduct))
(* Note: red_in_concl includes betaiotazeta and this was like *)
(* this since at least V6.3 (a pity *)
(* that intro do betaiotazeta only when reduction is needed; and *)
@@ -1035,7 +1043,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
(intro_then_gen name_flag move_flag false dep_flag tac))
begin function (e, info) -> match e with
| RefinerError (env, sigma, IntroNeedsProduct) ->
- Tacticals.New.tclZEROMSG (str "No product even after head-reduction.")
+ Tacticals.New.tclZEROMSG ~info (str "No product even after head-reduction.")
| e -> Proofview.tclZERO ~info e
end
end
@@ -1314,12 +1322,13 @@ let cut c =
know the relevance *)
match Typing.sort_of env sigma c with
| exception e when noncritical e ->
- Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
+ let _, info = Exninfo.capture e in
+ Tacticals.New.tclZEROMSG ~info (str "Not a proposition or a type.")
| sigma, s ->
let r = Sorts.relevance_of_sort s in
let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in
(* Backward compat: normalize [c]. *)
- let c = if normalize_cut then local_strong whd_betaiota sigma c else c in
+ let c = if normalize_cut then strong whd_betaiota env sigma c else c in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Refine.refine ~typecheck:false begin fun h ->
let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in
@@ -1607,7 +1616,7 @@ let make_projection env sigma params cstr sign elim i n c u =
noccur_between sigma 1 (n-i-1) t
(* to avoid surprising unifications, excludes flexible
projection types or lambda which will be instantiated by Meta/Evar *)
- && not (isEvar sigma (fst (whd_betaiota_stack sigma t)))
+ && not (isEvar sigma (fst (whd_betaiota_stack env sigma t)))
&& (accept_universal_lemma_under_conjunctions () || not (isRel sigma t))
then
let t = lift (i+1-n) t in
@@ -1666,7 +1675,9 @@ let descend_in_conjunctions avoid tac (err, info) c =
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
match make_projection env sigma params cstr sign elim i n c u with
- | None -> Tacticals.New.tclFAIL 0 (mt())
+ | None ->
+ let info = Exninfo.reify () in
+ Tacticals.New.tclFAIL ~info 0 (mt())
| Some (p,pt) ->
Tacticals.New.tclTHENS
(assert_before_gen false (NamingAvoid avoid) pt)
@@ -1718,7 +1729,8 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in
Clenvtac.res_pf clause ~with_evars ~flags
with exn when noncritical exn ->
- Proofview.tclZERO exn
+ let exn, info = Exninfo.capture exn in
+ Proofview.tclZERO ~info exn
in
let rec try_red_apply thm_ty (exn0, info) =
try
@@ -1730,9 +1742,10 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
| PretypeError _|RefinerError _|UserError _|Failure _ ->
Some (try_red_apply red_thm (exn0, info))
| _ -> None)
- with Redelimination ->
+ with Redelimination as exn ->
(* Last chance: if the head is a variable, apply may try
second order unification *)
+ let exn, info = Exninfo.capture exn in
let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in
let tac =
if with_destruct then
@@ -1991,7 +2004,9 @@ let assumption =
if only_eq then
let hyps = Proofview.Goal.hyps gl in
arec gl false hyps
- else Tacticals.New.tclZEROMSG (str "No such assumption.")
+ else
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (str "No such assumption.")
| decl::rest ->
let t = NamedDecl.get_type decl in
let concl = Proofview.Goal.concl gl in
@@ -2087,12 +2102,13 @@ let clear_body ids =
else sigma
in
Proofview.Unsafe.tclEVARS sigma
- with DependsOnBody where ->
+ with DependsOnBody where as exn ->
+ let _, info = Exninfo.capture exn in
let msg = match where with
| None -> str "Conclusion" ++ on_the_bodies ids
| Some id -> str "Hypothesis " ++ Id.print id ++ on_the_bodies ids
in
- Tacticals.New.tclZEROMSG msg
+ Tacticals.New.tclZEROMSG ~info msg
in
check <*>
Refine.refine ~typecheck:false begin fun sigma ->
@@ -2306,7 +2322,8 @@ let intro_decomp_eq ?loc l thin tac id =
(fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l)
(eq,t,eq_args) (c, t)
| None ->
- Tacticals.New.tclZEROMSG (str "Not a primitive equality here.")
+ 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 =
@@ -3025,7 +3042,7 @@ let specialize (c,lbind) ipat =
let flags = { (default_unify_flags ()) with resolve_evars = true } in
let clause = clenv_unify_meta_types ~flags clause in
let sigma = clause.evd in
- let (thd,tstack) = whd_nored_stack sigma (clenv_value clause) in
+ let (thd,tstack) = whd_nored_stack env sigma (clenv_value clause) in
(* The completely applied term is (thd tstack), but tstack may
contain unsolved metas, so now we must reabstract them
args with there name to have
@@ -3992,13 +4009,14 @@ let specialize_eqs id =
(internal_cut true id ty')
(exact_no_check ((* refresh_universes_strict *) acc'))
else
- Tacticals.New.tclFAIL 0 (str "Nothing to do in hypothesis " ++ Id.print id)
+ let info = Exninfo.reify () in
+ Tacticals.New.tclFAIL ~info 0 (str "Nothing to do in hypothesis " ++ Id.print id)
end
let specialize_eqs id = Proofview.Goal.enter begin fun gl ->
let msg = str "Specialization not allowed on dependent hypotheses" in
Proofview.tclOR (clear [id])
- (fun _ -> Tacticals.New.tclZEROMSG msg) >>= fun () ->
+ (fun (_,info) -> Tacticals.New.tclZEROMSG ~info msg) >>= fun () ->
specialize_eqs id
end
@@ -4414,7 +4432,8 @@ let induction_without_atomization isrec with_evars elim names lid =
scheme.nargs + (if scheme.farg_in_concl then 1 else 0) in
if not (Int.equal (List.length lid) (scheme.nparams + nargs_indarg_farg))
then
- Tacticals.New.tclZEROMSG (msg_not_right_number_induction_arguments scheme)
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (msg_not_right_number_induction_arguments scheme)
else
let indvars,lid_params = List.chop nargs_indarg_farg lid in
(* terms to patternify we must patternify indarg or farg if present in concl *)
@@ -4528,7 +4547,8 @@ let guard_no_unifiable = Proofview.guard_no_unifiable >>= function
| Some l ->
Proofview.tclENV >>= function env ->
Proofview.tclEVARMAP >>= function sigma ->
- Proofview.tclZERO (RefinerError (env, sigma, UnresolvedBindings l))
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info (RefinerError (env, sigma, UnresolvedBindings l))
let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
id ((pending,(c0,lbind)),(eqname,names)) t0 inhyps cls tac =
@@ -4831,7 +4851,9 @@ let reflexivity_red allowred =
let sigma = Tacmach.New.project gl in
let concl = maybe_betadeltaiota_concl allowred gl in
match match_with_equality_type env sigma concl with
- | None -> Proofview.tclZERO NoEquationFound
+ | None ->
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info NoEquationFound
| Some _ -> one_constructor 1 NoBindings
end
@@ -4873,8 +4895,9 @@ let match_with_equation c =
try
let res = match_with_equation env sigma c in
Proofview.tclUNIT res
- with NoEquationFound ->
- Proofview.tclZERO NoEquationFound
+ with NoEquationFound as exn ->
+ let _, info = Exninfo.capture exn in
+ Proofview.tclZERO ~info NoEquationFound
let symmetry_red allowred =
Proofview.Goal.enter begin fun gl ->
@@ -4987,7 +5010,9 @@ let transitivity_red allowred t =
| Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t])
| None,eq,eq_kind ->
match t with
- | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.")
+ | None ->
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (str"etransitivity not supported for this relation.")
| Some t -> prove_transitivity eq eq_kind t
end
@@ -5005,8 +5030,8 @@ let transitivity t = transitivity_gen (Some t)
let intros_transitivity n = Tacticals.New.tclTHEN intros (transitivity_gen n)
let constr_eq ~strict x y =
- let fail = Tacticals.New.tclFAIL 0 (str "Not equal") in
- let fail_universes = Tacticals.New.tclFAIL 0 (str "Not equal (due to universes)") in
+ let fail ~info = Tacticals.New.tclFAIL ~info 0 (str "Not equal") in
+ let fail_universes ~info = Tacticals.New.tclFAIL ~info 0 (str "Not equal (due to universes)") in
Proofview.Goal.enter begin fun gl ->
let env = Tacmach.New.pf_env gl in
let evd = Tacmach.New.project gl in
@@ -5015,13 +5040,18 @@ let constr_eq ~strict x y =
let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in
if strict then
if Evd.check_constraints evd csts then Proofview.tclUNIT ()
- else fail_universes
+ else
+ let info = Exninfo.reify () in
+ fail_universes ~info
else
(match Evd.add_constraints evd csts with
| evd -> Proofview.Unsafe.tclEVARS evd
- | exception Univ.UniverseInconsistency _ ->
- fail_universes)
- | None -> fail
+ | exception (Univ.UniverseInconsistency _ as e) ->
+ let _, info = Exninfo.capture e in
+ fail_universes ~info)
+ | None ->
+ let info = Exninfo.reify () in
+ fail ~info
end
let unify ?(state=TransparentState.full) x y =
@@ -5042,9 +5072,84 @@ let unify ?(state=TransparentState.full) x y =
let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in
Proofview.Unsafe.tclEVARS sigma
with e when noncritical e ->
- Proofview.tclZERO (PretypeError (env, sigma, CannotUnify (x, y, None)))
+ let e, info = Exninfo.capture e in
+ Proofview.tclZERO ~info (PretypeError (env, sigma, CannotUnify (x, y, None)))
end
+(** [tclWRAPFINALLY before tac finally] runs [before] before each
+ entry-point of [tac] and passes the result of [before] to
+ [finally], which is then run at each exit-point of [tac],
+ regardless of whether it succeeds or fails. Said another way, if
+ [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun
+ ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with
+ [e], it behaves as [before >>= fun v -> finally v <*> tclZERO
+ e]. Note that if [tac] succeeds [n] times before finally failing,
+ [before] and [finally] are both run [n+1] times (once around each
+ succuess, and once more around the final failure). *)
+(* We should probably export this somewhere, but it's not clear
+ where. As per
+ https://github.com/coq/coq/pull/12197#discussion_r418480525 and
+ https://gitter.im/coq/coq?at=5ead5c35347bd616304e83ef, we don't
+ export it from Proofview, because it seems somehow not primitive
+ enough. We don't export it from this file because it is more of a
+ tactical than a tactic. But we also don't export it from Tacticals
+ because all of the non-New tacticals there operate on `tactic`, not
+ `Proofview.tactic`, and all of the `New` tacticals that deal with
+ multi-success things are focussing, i.e., apply their arguments on
+ each goal separately (and it even says so in the comment on `New`),
+ whereas it's important that `tclWRAPFINALLY` doesn't introduce
+ extra focussing. *)
+let rec tclWRAPFINALLY before tac finally =
+ let open Proofview in
+ let open Proofview.Notations in
+ before >>= fun v -> tclCASE tac >>= function
+ | Fail (e, info) -> finally v >>= fun () -> tclZERO ~info e
+ | Next (ret, tac') -> tclOR
+ (finally v >>= fun () -> tclUNIT ret)
+ (fun e -> tclWRAPFINALLY before (tac' e) finally)
+
+let with_set_strategy lvl_ql k =
+ let glob_key r =
+ match r with
+ | GlobRef.ConstRef sp -> ConstKey sp
+ | GlobRef.VarRef id -> VarKey id
+ | _ -> user_err Pp.(str
+ "cannot set an inductive type or a constructor as transparent") in
+ let kl = List.concat (List.map (fun (lvl, ql) -> List.map (fun q -> (lvl, glob_key q)) ql) lvl_ql) in
+ tclWRAPFINALLY
+ (Proofview.tclENV >>= fun env ->
+ let orig_kl = List.map (fun (_lvl, k) ->
+ (Conv_oracle.get_strategy (Environ.oracle env) k, k))
+ kl in
+ (* Because the global env might be desynchronized from the
+ proof-local env, we need to update the global env to have this
+ tactic play nicely with abstract.
+ TODO: When abstract no longer depends on Global, delete this
+ let orig_kl_global = ... in *)
+ let orig_kl_global = List.map (fun (_lvl, k) ->
+ (Conv_oracle.get_strategy (Environ.oracle (Global.env ())) k, k))
+ kl in
+ let env = List.fold_left (fun env (lvl, k) ->
+ Environ.set_oracle env
+ (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env kl in
+ Proofview.Unsafe.tclSETENV env <*>
+ (* TODO: When abstract no longer depends on Global, remove this
+ [Proofview.tclLIFT] block *)
+ Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+ List.iter (fun (lvl, k) -> Global.set_strategy k lvl) kl)) <*>
+ Proofview.tclUNIT (orig_kl, orig_kl_global))
+ k
+ (fun (orig_kl, orig_kl_global) ->
+ (* TODO: When abstract no longer depends on Global, remove this
+ [Proofview.tclLIFT] block *)
+ Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+ List.iter (fun (lvl, k) -> Global.set_strategy k lvl) orig_kl_global)) <*>
+ Proofview.tclENV >>= fun env ->
+ let env = List.fold_left (fun env (lvl, k) ->
+ Environ.set_oracle env
+ (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env orig_kl in
+ Proofview.Unsafe.tclSETENV env)
+
module Simple = struct
(** Simplified version of some of the above tactics *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c84ba17f23..b6eb48a3d9 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -435,6 +435,12 @@ val declare_intro_decomp_eq :
(types * constr * constr) ->
constr * types -> unit Proofview.tactic) -> unit
+(** Tactic analogous to the [Strategy] vernacular, but only applied
+ locally to the tactic argument *)
+val with_set_strategy :
+ (Conv_oracle.level * Names.GlobRef.t list) list ->
+ 'a Proofview.tactic -> 'a Proofview.tactic
+
(** {6 Simple form of basic tactics. } *)
module Simple : sig
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 14:09:25 +0000