aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml6
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/class_tactics.ml10
-rw-r--r--tactics/eauto.ml6
-rw-r--r--tactics/eqschemes.ml2
-rw-r--r--tactics/equality.ml2
-rw-r--r--tactics/hints.ml6
-rw-r--r--tactics/hipattern.ml4
-rw-r--r--tactics/inv.ml4
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/tactic_matching.ml2
-rw-r--r--tactics/tacticals.ml8
-rw-r--r--tactics/tactics.ml22
13 files changed, 38 insertions, 38 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6c1f38d48..962af4b5c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -10,7 +10,7 @@
*)
open Pp
open Util
-open Errors
+open CErrors
open Names
open Vars
open Termops
@@ -222,7 +222,7 @@ let tclLOG (dbg,depth,trace) pp tac =
Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)");
out
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
iraise reraise
end
@@ -234,7 +234,7 @@ let tclLOG (dbg,depth,trace) pp tac =
trace := (depth, Some pp) :: !trace;
out
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
trace := (depth, None) :: !trace;
iraise reraise
end
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 9ae0ab90b..475005648 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -13,7 +13,7 @@ open Tacticals
open Tactics
open Term
open Termops
-open Errors
+open CErrors
open Util
open Mod_subst
open Locus
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 63b5e2a70..6e01a676a 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -13,7 +13,7 @@
*)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -382,7 +382,7 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
if cl.cl_strict then
Evd.evars_of_term concl
else Evar.Set.empty
- with e when Errors.noncritical e -> Evar.Set.empty
+ with e when CErrors.noncritical e -> Evar.Set.empty
in
let hintl =
List.map_append
@@ -485,7 +485,7 @@ let is_unique env concl =
try
let (cl,u), args = dest_class_app env concl in
cl.cl_unique
- with e when Errors.noncritical e -> false
+ with e when CErrors.noncritical e -> false
(** Sort the undefined variables from the least-dependent to most dependent. *)
let top_sort evm undefs =
@@ -1288,7 +1288,7 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state)
~depth dbs =
let dbs = List.map_filter
(fun db -> try Some (searchtable_map db)
- with e when Errors.noncritical e -> None)
+ with e when CErrors.noncritical e -> None)
dbs
in
let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
@@ -1444,7 +1444,7 @@ let resolve_typeclass_evars debug depth unique env evd filter split fail =
let evd =
try Evarconv.consider_remaining_unif_problems
~ts:(Typeclasses.classes_transparent_state ()) env evd
- with e when Errors.noncritical e -> evd
+ with e when CErrors.noncritical e -> evd
in
resolve_all_evars debug depth unique env
(initial_select_evars filter) evd split fail
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 93c201bf1..2eca1e597 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -231,8 +231,8 @@ module SearchProblem = struct
(* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
(* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
(lgls, cost, pptac) :: aux tacl
- with e when Errors.noncritical e ->
- let e = Errors.push e in
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in
Refiner.catch_failerror e; aux tacl
in aux l
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index a03489c80..1a45217a4 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -44,7 +44,7 @@
natural expectation of the user.
*)
-open Errors
+open CErrors
open Util
open Names
open Term
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 24028b09d..f18de92c0 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2c2b76412..8f3eb5eb5 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -8,7 +8,7 @@
open Pp
open Util
-open Errors
+open CErrors
open Names
open Vars
open Term
@@ -1273,7 +1273,7 @@ let pr_hint h = match h.obj with
try
let (_, env) = Pfedit.get_current_goal_context () in
env
- with e when Errors.noncritical e -> Global.env ()
+ with e when CErrors.noncritical e -> Global.env ()
in
(str "(*external*) " ++ Pptactic.pr_glb_generic env tac)
@@ -1334,7 +1334,7 @@ let pr_applicable_hint () =
let pts = get_pftreestate () in
let glss = Proof.V82.subgoals pts in
match glss.Evd.it with
- | [] -> Errors.error "No focused goal."
+ | [] -> CErrors.error "No focused goal."
| g::_ ->
pr_hint_term (Goal.V82.concl glss.Evd.sigma g)
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index f2c72c2f3..6e24cc469 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -409,7 +409,7 @@ let rec first_match matcher = function
let match_eq eqn (ref, hetero) =
let ref =
try Lazy.force ref
- with e when Errors.noncritical e -> raise PatternMatchingFailure
+ with e when CErrors.noncritical e -> raise PatternMatchingFailure
in
match kind_of_term eqn with
| App (c, [|t; x; y|]) ->
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 852c2ee7c..bda16b01c 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -440,7 +440,7 @@ let raw_inversion inv_kind id status names =
try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c)
with UserError _ ->
let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in
- Errors.errorlabstrm "" msg
+ CErrors.errorlabstrm "" msg
in
let IndType (indf,realargs) = find_rectype env sigma t in
let evdref = ref sigma in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 63b1a7b54..642bf520b 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
diff --git a/tactics/tactic_matching.ml b/tactics/tactic_matching.ml
index 2144b75e7..004492e78 100644
--- a/tactics/tactic_matching.ml
+++ b/tactics/tactic_matching.ml
@@ -103,7 +103,7 @@ let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) =
(merged, Id.Map.merge merge lcm lm)
let matching_error =
- Errors.UserError ("tactic matching" , Pp.str "No matching clauses for match.")
+ CErrors.UserError ("tactic matching" , Pp.str "No matching clauses for match.")
let imatching_error = (matching_error, Exninfo.null)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 46145d111..87fdcf14d 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -521,7 +521,7 @@ module New = struct
try
let () = check_evars env sigma_final sigma sigma_initial in
tclUNIT x
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
tclZERO e
else
tclUNIT x
@@ -540,7 +540,7 @@ module New = struct
Proofview.tclOR
(Proofview.tclTIMEOUT n t)
begin function (e, info) -> match e with
- | Proofview.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (Errors.print e)))
+ | Proofview.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (CErrors.print e)))
| e -> Proofview.tclZERO ~info e
end
@@ -551,7 +551,7 @@ module New = struct
let hyps = Proofview.Goal.hyps gl in
try
List.nth hyps (m-1)
- with Failure _ -> Errors.error "No such assumption."
+ with Failure _ -> CErrors.error "No such assumption."
let nLastDecls gl n =
try List.firstn n (Proofview.Goal.hyps gl)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 61aaef871..e48901314 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -350,7 +350,7 @@ let rename_hyp repl =
let () =
try
let elt = Id.Set.choose (Id.Set.inter dst mods) in
- Errors.errorlabstrm "" (pr_id elt ++ str " is already used")
+ CErrors.errorlabstrm "" (pr_id elt ++ str " is already used")
with Not_found -> ()
in
(** All is well *)
@@ -1807,8 +1807,8 @@ let apply_in_once_main flags innerclause env sigma (d,lbind) =
let thm = nf_betaiota sigma (Retyping.get_type_of env sigma d) in
let rec aux clause =
try progress_with_clause flags innerclause clause
- with e when Errors.noncritical e ->
- let e = Errors.push e in
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in
try aux (clenv_push_prod clause)
with NotExtensibleClause -> iraise e
in
@@ -1838,8 +1838,8 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
clear idstoclear;
tac id
])
- with e when with_destruct && Errors.noncritical e ->
- let (e, info) = Errors.push e in
+ with e when with_destruct && CErrors.noncritical e ->
+ let (e, info) = CErrors.push e in
(descend_in_conjunctions [targetid]
(fun b id -> aux (id::idstoclear) b (mkVar id))
(e, info) c)
@@ -1987,7 +1987,7 @@ let check_is_type env sigma ty =
try
let _ = Typing.e_sort_of env evdref ty in
!evdref
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
raise (DependsOnBody None)
let check_decl env sigma decl =
@@ -2001,7 +2001,7 @@ let check_decl env sigma decl =
| LocalDef (_,c,_) -> Typing.e_check env evdref c ty
in
!evdref
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
let id = get_id decl in
raise (DependsOnBody (Some id))
@@ -3880,7 +3880,7 @@ let compute_elim_sig ?elimc elimt =
| Some (LocalAssum (_,ind)) ->
let indhd,indargs = decompose_app ind in
try {!res with indref = Some (global_of_constr indhd) }
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
error "Cannot find the inductive type of the inductive scheme."
let compute_scheme_signature scheme names_info ind_type_guess =
@@ -4851,7 +4851,7 @@ let abstract_subproof id gk tac =
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) = Errors.push src in
+ let (_, info) = CErrors.push src in
iraise (e, info)
in
let const, args =
@@ -4911,7 +4911,7 @@ let unify ?(state=full_transparent_state) x y =
let sigma = Sigma.to_evar_map sigma in
let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in
Sigma.Unsafe.of_pair (Proofview.tclUNIT (), sigma)
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
Sigma.here (Tacticals.New.tclFAIL 0 (str"Not unifiable")) sigma
end }
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 19:28:41 +0000