aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/classops.ml2
-rw-r--r--pretyping/coercion.ml4
-rw-r--r--pretyping/constr_matching.ml2
-rw-r--r--pretyping/detyping.ml6
-rw-r--r--pretyping/evarconv.ml4
-rw-r--r--pretyping/evarsolve.ml4
-rw-r--r--pretyping/find_subterm.ml2
-rw-r--r--pretyping/indrec.ml2
-rw-r--r--pretyping/inductiveops.ml2
-rw-r--r--pretyping/locusops.ml6
-rw-r--r--pretyping/nativenorm.ml10
-rw-r--r--pretyping/patternops.ml2
-rw-r--r--pretyping/pretype_errors.ml2
-rw-r--r--pretyping/pretyping.ml12
-rw-r--r--pretyping/program.ml2
-rw-r--r--pretyping/recordops.ml6
-rw-r--r--pretyping/redops.ml4
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--pretyping/retyping.ml2
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--pretyping/typeclasses.ml8
-rw-r--r--pretyping/typing.ml2
-rw-r--r--pretyping/unification.ml12
-rw-r--r--pretyping/vnorm.ml2
25 files changed, 53 insertions, 53 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c39a57012..985ad4b0d 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 5fb6c130e..4f265e76c 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Pp
open Flags
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 704559dd7..913e80f39 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -14,7 +14,7 @@
Corbineau, Feb 2008 *)
(* Turned into an abstract compilation unit by Matthieu Sozeau, March 2006 *)
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -370,7 +370,7 @@ let apply_coercion env sigma p hj typ_cl =
(hj,typ_cl,sigma) p
in evd, j
with NoCoercion as e -> raise e
- | e when Errors.noncritical e -> anomaly (Pp.str "apply_coercion")
+ | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion")
(* Try to coerce to a funclass; raise NoCoercion if not possible *)
let inh_app_fun_core env evd j =
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index c566839e8..886a98263 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -8,7 +8,7 @@
(*i*)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Globnames
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index cc178eb97..d4066f387 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -323,7 +323,7 @@ let is_nondep_branch c l =
(* FIXME: do better using tags from l *)
let sign,ccl = decompose_lam_n_decls (List.length l) c in
noccur_between 1 (Context.Rel.length sign) ccl
- with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *)
+ with e when CErrors.noncritical e -> (* Not eta-expanded or not reduced *)
false
let extract_nondep_branches test c b l =
@@ -631,7 +631,7 @@ and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl =
let mat = build_tree Anonymous (snd flags) (avoid,env) ci bl in
List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype flags avoid env sigma c))
mat
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
Array.to_list
(Array.map3 (detype_eqn flags avoid env sigma) constructs consnargsl bl)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 729006dbb..8abe6116b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -766,7 +766,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
in Success evd'
with Univ.UniverseInconsistency p ->
UnifFailure (evd,UnifUnivInconsistency p)
- | e when Errors.noncritical e -> UnifFailure (evd,NotSameHead))
+ | e when CErrors.noncritical e -> UnifFailure (evd,NotSameHead))
| Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty ->
ise_and evd
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 77b0c67ad..62700aef3 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Util
-open Errors
+open CErrors
open Names
open Term
open Vars
@@ -1460,7 +1460,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
imitate envk t in
t::l
- with e when Errors.noncritical e -> l in
+ with e when CErrors.noncritical e -> l in
(match candidates with
| [x] -> x
| _ ->
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index df1fc20f1..4caa1e992 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -8,7 +8,7 @@
open Pp
open Util
-open Errors
+open CErrors
open Names
open Locus
open Term
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 866b2b495..0c80bd019 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -11,7 +11,7 @@
(* This file builds various inductive schemes *)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Libnames
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 6be6a2d3a..fbad0d949 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Names
open Univ
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index d89aeccd8..e4fbf8d54 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -50,9 +50,9 @@ let is_nowhere = function
let simple_clause_of enum_hyps cl =
let error_occurrences () =
- Errors.error "This tactic does not support occurrences selection" in
+ CErrors.error "This tactic does not support occurrences selection" in
let error_body_selection () =
- Errors.error "This tactic does not support body selection" in
+ CErrors.error "This tactic does not support body selection" in
let hyps =
match cl.onhyps with
| None ->
@@ -84,7 +84,7 @@ let concrete_clause_of enum_hyps cl =
(** Miscellaneous functions *)
let out_arg = function
- | Misctypes.ArgVar _ -> Errors.anomaly (Pp.str "Unevaluated or_var variable")
+ | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable")
| Misctypes.ArgArg x -> x
let occurrences_of_hyp id cls =
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index e537a3c0a..0dd64697c 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Term
open Vars
open Environ
@@ -178,7 +178,7 @@ let rec nf_val env v typ =
let name,dom,codom =
try decompose_prod env typ
with DestKO ->
- Errors.anomaly
+ CErrors.anomaly
(Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
in
let env = push_rel (LocalAssum (name,dom)) env in
@@ -224,7 +224,7 @@ and nf_args env accu t =
let _,dom,codom =
try decompose_prod env t with
DestKO ->
- Errors.anomaly
+ CErrors.anomaly
(Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
in
let c = nf_val env arg dom in
@@ -241,7 +241,7 @@ and nf_bargs env b t =
let _,dom,codom =
try decompose_prod env !t with
DestKO ->
- Errors.anomaly
+ CErrors.anomaly
(Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
in
let c = nf_val env (block_field b i) dom in
@@ -352,7 +352,7 @@ and nf_predicate env ind mip params v pT =
let name,dom,codom =
try decompose_prod env pT with
DestKO ->
- Errors.anomaly
+ CErrors.anomaly
(Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
in
let dep,body =
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 7eb3d633d..fe73b6105 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Names
open Globnames
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index b0715af73..00b6100c0 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -60,7 +60,7 @@ type pretype_error =
exception PretypeError of env * Evd.evar_map * pretype_error
let precatchable_exception = function
- | Errors.UserError _ | TypeError _ | PretypeError _
+ | CErrors.UserError _ | TypeError _ | PretypeError _
| Nametab.GlobalizationError _ -> true
| _ -> false
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 38defe951..c8f61c66b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -22,7 +22,7 @@
open Pp
-open Errors
+open CErrors
open Util
open Names
open Evd
@@ -81,7 +81,7 @@ let search_guard loc env possible_indexes fixdefs =
let fix = ((indexes, 0),fixdefs) in
(try check_fix env fix
with reraise ->
- let (e, info) = Errors.push reraise in
+ let (e, info) = CErrors.push reraise in
let info = Loc.add_loc info loc in
iraise (e, info));
indexes
@@ -228,8 +228,8 @@ let apply_heuristics env evdref fail_evar =
(* Resolve eagerly, potentially making wrong choices *)
try evdref := consider_remaining_unif_problems
~ts:(Typeclasses.classes_transparent_state ()) env !evdref
- with e when Errors.noncritical e ->
- let e = Errors.push e in if fail_evar then iraise e
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in if fail_evar then iraise e
let check_typeclasses_instances_are_solved env current_sigma frozen =
(* Naive way, call resolution again with failure flag *)
@@ -624,7 +624,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
let cofix = (i,(names,ftys,fdefs)) in
(try check_cofix env cofix
with reraise ->
- let (e, info) = Errors.push reraise in
+ let (e, info) = CErrors.push reraise in
let info = Loc.add_loc info loc in
iraise (e, info));
make_judge (mkCoFix cofix) ftys.(i)
@@ -757,7 +757,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
try
judge_of_product env name j j'
with TypeError _ as e ->
- let (e, info) = Errors.push e in
+ let (e, info) = CErrors.push e in
let info = Loc.add_loc info loc in
iraise (e, info) in
inh_conv_coerce_to_tycon loc env evdref resj tycon
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 253d85742..b4333847b 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 95c6725f3..682a88333 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -13,7 +13,7 @@
(* This file registers properties of records: projections and
canonical structures *)
-open Errors
+open CErrors
open Util
open Pp
open Names
@@ -176,7 +176,7 @@ let cs_pattern_of_constr t =
App (f,vargs) ->
begin
try Const_cs (global_of_constr f) , None, Array.to_list vargs
- with e when Errors.noncritical e -> raise Not_found
+ with e when CErrors.noncritical e -> raise Not_found
end
| Rel n -> Default_cs, Some n, []
| Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, None, [a; Termops.pop b]
@@ -184,7 +184,7 @@ let cs_pattern_of_constr t =
| _ ->
begin
try Const_cs (global_of_constr t) , None, []
- with e when Errors.noncritical e -> raise Not_found
+ with e when CErrors.noncritical e -> raise Not_found
end
let warn_projection_no_head_constant =
diff --git a/pretyping/redops.ml b/pretyping/redops.ml
index db5879174..7d65925e5 100644
--- a/pretyping/redops.ml
+++ b/pretyping/redops.ml
@@ -20,12 +20,12 @@ let make_red_flag l =
| FZeta :: lf -> add_flag { red with rZeta = true } lf
| FConst l :: lf ->
if red.rDelta then
- Errors.error
+ CErrors.error
"Cannot set both constants to unfold and constants not to unfold";
add_flag { red with rConst = union_consts red.rConst l } lf
| FDeltaBut l :: lf ->
if red.rConst <> [] && not red.rDelta then
- Errors.error
+ CErrors.error
"Cannot set both constants to unfold and constants not to unfold";
add_flag
{ red with rConst = union_consts red.rConst l; rDelta = true }
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 29b448caa..76c4304c4 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -1206,7 +1206,7 @@ let pb_equal = function
let report_anomaly _ =
let e = UserError ("", Pp.str "Conversion test raised an anomaly") in
- let e = Errors.push e in
+ let e = CErrors.push e in
iraise e
let test_trans_conversion (f: constr Reduction.extended_conversion_function) reds env sigma x y =
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 5de540a00..98b36fb92 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Term
open Vars
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 51a89966f..2d07bf4d5 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d57eef2e1..2c675b9ea 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -150,7 +150,7 @@ let dest_class_arity env c =
let class_of_constr c =
try Some (dest_class_arity (Global.env ()) c)
- with e when Errors.noncritical e -> None
+ with e when CErrors.noncritical e -> None
let is_class_constr c =
try let gr, u = Universes.global_of_constr c in
@@ -249,7 +249,7 @@ let rebuild_class cl =
try
let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in
set_typeclass_transparency cst false false; cl
- with e when Errors.noncritical e -> cl
+ with e when CErrors.noncritical e -> cl
let class_input : typeclass -> obj =
declare_object
@@ -272,7 +272,7 @@ let check_instance env sigma c =
let (evd, c) = resolve_one_typeclass env sigma
(Retyping.get_type_of env sigma c) in
not (Evd.has_undefined evd)
- with e when Errors.noncritical e -> false
+ with e when CErrors.noncritical e -> false
let build_subclasses ~check env sigma glob pri =
let _id = Nametab.basename_of_global glob in
@@ -422,7 +422,7 @@ let add_class cl =
match inst with
| Some (Backward, pri) ->
(match body with
- | None -> Errors.error "Non-definable projection can not be declared as a subinstance"
+ | None -> CErrors.error "Non-definable projection can not be declared as a subinstance"
| Some b -> declare_instance pri false (ConstRef b))
| _ -> ())
cl.cl_projs
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 8e44fb008..0e4885bea 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Term
open Vars
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5bb853b69..c17879739 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Pp
open Util
open Names
@@ -742,7 +742,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
then Evd.set_leq_sort curenv sigma s1 s2
else Evd.set_eq_sort curenv sigma s1 s2
in (sigma', metasubst, evarsubst)
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
error_cannot_unify curenv sigma (m,n))
| Lambda (na,t1,c1), Lambda (_,t2,c2) ->
@@ -1138,11 +1138,11 @@ let merge_instances env sigma flags st1 st2 c1 c2 =
else (right, st2, res)
| (IsSuperType,IsSubType) ->
(try (left, IsSubType, unify_0 env sigma CUMUL flags c2 c1)
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
(right, IsSubType, unify_0 env sigma CUMUL flags c1 c2))
| (IsSubType,IsSuperType) ->
(try (left, IsSuperType, unify_0 env sigma CUMUL flags c1 c2)
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
(right, IsSuperType, unify_0 env sigma CUMUL flags c2 c1))
(* Unification
@@ -1353,7 +1353,7 @@ let w_merge env with_types flags (evd,metas,evars) =
let rec process_eqns failures = function
| (mv,status,c)::eqns ->
(match (try Inl (unify_type env evd flags mv status c)
- with e when Errors.noncritical e -> Inr e)
+ with e when CErrors.noncritical e -> Inr e)
with
| Inr e -> process_eqns (((mv,status,c),e)::failures) eqns
| Inl (evd,metas,evars) ->
@@ -1555,7 +1555,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
| PretypeError (_,_,CannotUnify (c1,c2,Some e)) ->
raise (NotUnifiable (Some (c1,c2,e)))
(** MS: This is pretty bad, it catches Not_found for example *)
- | e when Errors.noncritical e -> raise (NotUnifiable None) in
+ | e when CErrors.noncritical e -> raise (NotUnifiable None) in
let merge_fun c1 c2 =
match c1, c2 with
| Some (evd,c1,x), Some (_,c2,_) ->
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 0b102f921..c396f593b 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -305,7 +305,7 @@ and nf_fun env f typ =
try decompose_prod env typ
with DestKO ->
(* 27/2/13: Turned this into an anomaly *)
- Errors.anomaly
+ CErrors.anomaly
(Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
in
let body = nf_val (push_rel (LocalAssum (name,dom)) env) vb codom in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 20:27:45 +0000