aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/abstract.ml4
-rw-r--r--tactics/class_tactics.ml7
-rw-r--r--tactics/eauto.ml2
-rw-r--r--tactics/hints.ml11
-rw-r--r--tactics/hints.mli2
-rw-r--r--tactics/pfedit.ml8
-rw-r--r--tactics/tacticals.mli2
-rw-r--r--tactics/tactics.ml25
8 files changed, 36 insertions, 25 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 1e18028e7b..86e6a92a22 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -97,8 +97,8 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
which is an error irrelevant to the proof system (in fact it
means that [e] comes from [tac] failing to yield enough
success). Hence it reraises [e]. *)
- let (_, info) = CErrors.push src in
- iraise (e, info)
+ let (_, info) = Exninfo.capture src in
+ Exninfo.iraise (e, info)
in
let body, effs = Future.force const.Declare.proof_entry_body in
(* We drop the side-effects from the entry, they already exist in the ambient environment *)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 28feeecb86..e3f2f18b44 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -236,7 +236,7 @@ let unify_resolve_refine poly flags gl clenv =
Tacticals.New.tclZEROMSG (str "Unable to unify")
| e when CErrors.noncritical e ->
Tacticals.New.tclZEROMSG (str "Unexpected error")
- | _ -> iraise ie)
+ | _ -> Exninfo.iraise ie)
(** Dealing with goals of the form A -> B and hints of the form
C -> A -> B.
@@ -528,9 +528,10 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
let hints = build_subclasses ~check:false env sigma (GlobRef.VarRef id) empty_hint_info in
(List.map_append
(fun (path,info,c) ->
+ let h = IsConstr (EConstr.of_constr c,Univ.ContextSet.empty) [@ocaml.warning "-3"] in
make_resolves env sigma ~name:(PathHints path)
(true,false,not !Flags.quiet) info ~poly:false
- (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty)))
+ h)
hints)
else []
in
@@ -770,7 +771,7 @@ module Search = struct
(fun e' ->
if CErrors.noncritical (fst e') then
(pr_error e'; aux (merge_exceptions e e') tl)
- else iraise e')
+ else Exninfo.iraise e')
and aux e = function
| x :: xs -> onetac e x xs
| [] ->
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 9a1e6a6736..aca6b4734a 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -235,7 +235,7 @@ module SearchProblem = struct
(* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
(lgls, cost, pptac) :: aux tacl
with e when CErrors.noncritical e ->
- let e = CErrors.push e in
+ let e = Exninfo.capture e in
Refiner.catch_failerror e; aux tacl
in aux l
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 86aa046586..731792e34e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1325,6 +1325,13 @@ let project_hint ~poly pri l2r r =
let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
(info,false,true,PathAny, IsGlobRef (GlobRef.ConstRef c))
+let warn_deprecated_hint_constr =
+ CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated"
+ (fun () ->
+ Pp.strbrk
+ "Declaring arbitrary terms as hints is deprecated; declare a global reference instead"
+ )
+
let interp_hints ~poly =
fun h ->
let env = Global.env () in
@@ -1349,7 +1356,9 @@ let interp_hints ~poly =
| HintsReference c ->
let gr = global_with_alias c in
(PathHints [gr], poly, IsGlobRef gr)
- | HintsConstr c -> (PathAny, poly, f poly c)
+ | HintsConstr c ->
+ let () = warn_deprecated_hint_constr () in
+ (PathAny, poly, f poly c)
in
let fp = Constrintern.intern_constr_pattern env sigma in
let fres (info, b, r) =
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 9c9f0b7708..7bb17489bf 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -181,7 +181,7 @@ type hnf = bool
type hint_term =
| IsGlobRef of GlobRef.t
- | IsConstr of constr * Univ.ContextSet.t
+ | IsConstr of constr * Univ.ContextSet.t [@ocaml.deprecated "Declare a hint constant instead"]
type hints_entry =
| HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index dbabc4e4e0..7cdfd0637a 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -130,8 +130,8 @@ let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ctx sign ~
| _ ->
CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
with reraise ->
- let reraise = CErrors.push reraise in
- iraise reraise
+ let reraise = Exninfo.capture reraise in
+ Exninfo.iraise reraise
let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac =
let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
@@ -160,8 +160,8 @@ let refine_by_tactic ~name ~poly env sigma ty tac =
try Proof.run_tactic env tac prf
with Logic_monad.TacticFailure e as src ->
(* Catch the inner error of the monad tactic *)
- let (_, info) = CErrors.push src in
- iraise (e, info)
+ let (_, info) = Exninfo.capture src in
+ Exninfo.iraise (e, info)
in
(* Plug back the retrieved sigma *)
let Proof.{ goals; stack; shelf; given_up; sigma; entry } = Proof.data prf in
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 4b93b81d1c..5fde6d2178 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -144,7 +144,7 @@ module New : sig
(** [catch_failerror e] fails and decreases the level if [e] is an
Ltac error with level more than 0. Otherwise succeeds. *)
- val catch_failerror : Util.iexn -> unit tactic
+ val catch_failerror : Exninfo.iexn -> unit tactic
val tclIDTAC : unit tactic
val tclTHEN : unit tactic -> unit tactic -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8371da76b2..ef50c56dc4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1848,12 +1848,12 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) =
let rec aux clause =
try progress_with_clause flags innerclause clause
with e when CErrors.noncritical e ->
- let e' = CErrors.push e in
+ let e' = Exninfo.capture e in
try aux (clenv_push_prod clause)
with NotExtensibleClause ->
match e with
| UnableToApply -> explain_unable_to_apply_lemma ?loc env sigma thm innerclause
- | _ -> iraise e'
+ | _ -> Exninfo.iraise e'
in
aux (make_clenv_binding env sigma (d,thm) lbind)
@@ -1886,7 +1886,7 @@ let apply_in_once ?(respect_opaque = false) with_delta
tac id
])
with e when with_destruct && CErrors.noncritical e ->
- let (e, info) = CErrors.push e in
+ let (e, info) = Exninfo.capture e in
(descend_in_conjunctions (Id.Set.singleton targetid)
(fun b id -> aux (id::idstoclear) b (mkVar id))
(e, info) c)
@@ -3155,7 +3155,7 @@ let clear_for_destruct ids =
(clear_gen (fun env sigma id err inglobal -> raise (ClearDependencyError (id,err,inglobal))) ids)
(function
| ClearDependencyError (id,err,inglobal),_ -> warn_cannot_remove_as_expected (id,inglobal); Proofview.tclUNIT ()
- | e -> iraise e)
+ | e -> Exninfo.iraise e)
(* Either unfold and clear if defined or simply clear if not a definition *)
let expand_hyp id =
@@ -4246,25 +4246,26 @@ type eliminator_source =
| ElimOver of bool * Id.t
let find_induction_type isrec elim hyp0 gl =
- let sigma, scheme,elim =
+ let sigma, indref, nparams, elim =
match elim with
| None ->
let sort = Tacticals.New.elimination_sort_of_goal gl in
- let sigma, (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in
- let scheme = compute_elim_sig sigma ~elimc elimt in
- (* We drop the scheme waiting to know if it is dependent *)
- sigma, scheme, ElimOver (isrec,hyp0)
+ let sigma', (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in
+ let scheme = compute_elim_sig sigma' ~elimc elimt in
+ (* We drop the scheme and elimc/elimt waiting to know if it is dependent, this
+ needs no update to sigma at this point. *)
+ Tacmach.New.project gl, scheme.indref, scheme.nparams, ElimOver (isrec,hyp0)
| Some e ->
let sigma, (elimc,elimt),ind_guess = given_elim hyp0 e gl in
let scheme = compute_elim_sig sigma ~elimc elimt in
if Option.is_empty scheme.indarg then error "Cannot find induction type";
let indsign = compute_scheme_signature sigma scheme hyp0 ind_guess in
let elim = ({ elimindex = Some(-1); elimbody = elimc },elimt) in
- sigma, scheme, ElimUsing (elim,indsign)
+ sigma, scheme.indref, scheme.nparams, ElimUsing (elim,indsign)
in
- match scheme.indref with
+ match indref with
| None -> error_ind_scheme ""
- | Some ref -> sigma, (ref, scheme.nparams, elim)
+ | Some ref -> sigma, (ref, nparams, elim)
let get_elim_signature elim hyp0 gl =
compute_elim_signature (given_elim hyp0 elim gl) hyp0
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 19:43:06 +0000