diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 5 | ||||
| -rw-r--r-- | pretyping/pretype_errors.ml | 12 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 7 | ||||
| -rw-r--r-- | pretyping/typeclasses_errors.ml | 5 |
4 files changed, 16 insertions, 13 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 4b565ddbd9..1a30b4e2cf 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Util open Names open Nameops @@ -42,7 +43,7 @@ type pattern_matching_error = exception PatternMatchingError of env * pattern_matching_error let raise_pattern_matching_error (loc,ctx,te) = - Stdpp.raise_with_loc loc (PatternMatchingError(ctx,te)) + Loc.raise loc (PatternMatchingError(ctx,te)) let error_bad_pattern_loc loc cstr ind = raise_pattern_matching_error (loc, Global.env(), BadPattern (cstr,ind)) @@ -98,7 +99,7 @@ let rec list_try_compile f = function | h::t -> try f h with UserError _ | TypeError _ | PretypeError _ - | Stdpp.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) -> + | Loc.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) -> list_try_compile f t let force_name = diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 6adaee81c2..5b829e5bf4 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -6,8 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Compat open Util -open Stdpp open Names open Sign open Term @@ -41,7 +41,7 @@ exception PretypeError of env * pretype_error let precatchable_exception = function | Util.UserError _ | TypeError _ | PretypeError _ - | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | + | Loc.Exc_located(_,(Util.UserError _ | TypeError _ | Nametab.GlobalizationError _ | PretypeError _)) -> true | _ -> false @@ -96,10 +96,10 @@ let contract3 env a b c = match contract env [a;b;c] with | env, [a;b;c] -> env,a,b,c | _ -> assert false let raise_pretype_error (loc,ctx,sigma,te) = - Stdpp.raise_with_loc loc (PretypeError(env_ise sigma ctx,te)) + Loc.raise loc (PretypeError(env_ise sigma ctx,te)) let raise_located_type_error (loc,ctx,sigma,te) = - Stdpp.raise_with_loc loc (TypeError(env_ise sigma ctx,te)) + Loc.raise loc (TypeError(env_ise sigma ctx,te)) let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty = @@ -155,11 +155,11 @@ let error_occur_check env sigma ev c = let error_not_clean env sigma ev c (loc,k) = let c = nf_evar sigma c in - raise_with_loc loc + Loc.raise loc (PretypeError (env_ise sigma env, NotClean (ev,c,k))) let error_unsolvable_implicit loc env sigma evi e explain = - raise_with_loc loc + Loc.raise loc (PretypeError (env_ise sigma env, UnsolvableImplicit (evi, e, explain))) let error_cannot_unify env sigma (m,n) = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 70241238db..22a3451c4b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -21,6 +21,7 @@ (* Secondary maintenance: collective *) +open Compat open Pp open Util open Names @@ -66,7 +67,7 @@ let search_guard loc env possible_indexes fixdefs = let indexes = Array.of_list (List.map List.hd possible_indexes) in let fix = ((indexes, 0),fixdefs) in (try check_fix env fix with - | e -> if loc = dummy_loc then raise e else Stdpp.raise_with_loc loc e); + | e -> if loc = dummy_loc then raise e else Loc.raise loc e); indexes else (* we now search recursively amoungst all combinations *) @@ -396,7 +397,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | RCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e); + (try check_cofix env cofix with e -> Loc.raise loc e); make_judge (mkCoFix cofix) ftys.(i) in inh_conv_coerce_to_tycon loc env evdref fixj tycon @@ -464,7 +465,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct in let resj = try judge_of_product env name j j' - with TypeError _ as e -> Stdpp.raise_with_loc loc e in + with TypeError _ as e -> Loc.raise loc e in inh_conv_coerce_to_tycon loc env evdref resj tycon | RLetIn(loc,name,c1,c2) -> diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 869a7845d1..983942abad 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -16,6 +16,7 @@ open Environ open Nametab open Mod_subst open Topconstr +open Compat open Util open Libnames (*i*) @@ -45,7 +46,7 @@ let unsatisfiable_constraints env evd ev = raise (TypeClassError (env, UnsatisfiableConstraints (evd, None))) | Some ev -> let loc, kind = Evd.evar_source ev evd in - raise (Stdpp.Exc_located (loc, TypeClassError + raise (Loc.Exc_located (loc, TypeClassError (env, UnsatisfiableConstraints (evd, Some (ev, kind))))) let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m)) @@ -53,5 +54,5 @@ let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstan let rec unsatisfiable_exception exn = match exn with | TypeClassError (_, UnsatisfiableConstraints _) -> true - | Stdpp.Exc_located(_, e) -> unsatisfiable_exception e + | Loc.Exc_located(_, e) -> unsatisfiable_exception e | _ -> false |