aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/check.ml6
-rw-r--r--checker/checker.ml4
-rw-r--r--checker/environ.ml14
-rw-r--r--checker/indtypes.ml12
-rw-r--r--checker/inductive.ml16
-rw-r--r--checker/modops.ml16
-rw-r--r--checker/reduction.ml8
-rw-r--r--checker/safe_typing.ml4
-rw-r--r--checker/subtyping.ml8
-rw-r--r--checker/term.ml10
-rw-r--r--checker/typeops.ml6
-rw-r--r--checker/univ.ml16
12 files changed, 60 insertions, 60 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 11678fa6bb..b3b4034258 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -72,7 +72,7 @@ let find_library dir =
let try_find_library dir =
try find_library dir
with Not_found ->
- error ("Unknown library " ^ (DirPath.to_string dir))
+ user_err Pp.(str ("Unknown library " ^ (DirPath.to_string dir)))
let library_full_filename dir = (find_library dir).library_filename
@@ -165,7 +165,7 @@ let find_logical_path phys_dir =
match List.filter2 (fun p d -> p = phys_dir) physical logical with
| _,[dir] -> dir
| _,[] -> default_root_prefix
- | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir))
+ | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir^"."))
let remove_load_path dir =
let physical, logical = !load_paths in
@@ -197,7 +197,7 @@ let add_load_path (phys_path,coq_path) =
end
| _,[] ->
load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
- | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path))
+ | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path^"."))
let load_paths_of_dir_path dir =
let physical, logical = !load_paths in
diff --git a/checker/checker.ml b/checker/checker.ml
index 5cadfe7b94..e00f47a540 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -335,7 +335,7 @@ let parse_args argv =
| "-debug" :: rem -> set_debug (); parse rem
| "-where" :: _ ->
- Envars.set_coqlib ~fail:CErrors.error;
+ Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
print_endline (Envars.coqlib ());
exit 0
@@ -373,7 +373,7 @@ let init_with_argv argv =
try
parse_args argv;
if !Flags.debug then Printexc.record_backtrace true;
- Envars.set_coqlib ~fail:CErrors.error;
+ Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
if_verbose print_header ();
init_load_path ();
engage ();
diff --git a/checker/environ.ml b/checker/environ.ml
index 7b59c6b986..22d1eec178 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -45,7 +45,7 @@ let set_engagement (impr_set as c) env =
env.env_stratification.env_engagement in
begin
match impr_set,expected_impr_set with
- | PredicativeSet, ImpredicativeSet -> error "Incompatible engagement"
+ | PredicativeSet, ImpredicativeSet -> user_err Pp.(str "Incompatible engagement")
| _ -> ()
end;
{ env with env_stratification =
@@ -106,7 +106,7 @@ let anomaly s = anomaly (Pp.str s)
let add_constant kn cs env =
if Cmap_env.mem kn env.env_globals.env_constants then
- Printf.ksprintf anomaly ("Constant %s is already defined")
+ Printf.ksprintf anomaly ("Constant %s is already defined.")
(Constant.to_string kn);
let new_constants =
Cmap_env.add kn cs env.env_globals.env_constants in
@@ -161,7 +161,7 @@ let is_projection cst env =
let lookup_projection p env =
match (lookup_constant (Projection.constant p) env).const_proj with
| Some pb -> pb
- | None -> anomaly ("lookup_projection: constant is not a projection")
+ | None -> anomaly ("lookup_projection: constant is not a projection.")
(* Mutual Inductives *)
let scrape_mind env kn=
@@ -182,7 +182,7 @@ let lookup_mind kn env =
let add_mind kn mib env =
if Mindmap_env.mem kn env.env_globals.env_inductives then
- Printf.ksprintf anomaly ("Inductive %s is already defined")
+ Printf.ksprintf anomaly ("Inductive %s is already defined.")
(MutInd.to_string kn);
let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in
@@ -201,7 +201,7 @@ let add_mind kn mib env =
let add_modtype ln mtb env =
if MPmap.mem ln env.env_globals.env_modtypes then
- Printf.ksprintf anomaly ("Module type %s is already defined")
+ Printf.ksprintf anomaly ("Module type %s is already defined.")
(ModPath.to_string ln);
let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in
let new_globals =
@@ -211,7 +211,7 @@ let add_modtype ln mtb env =
let shallow_add_module mp mb env =
if MPmap.mem mp env.env_globals.env_modules then
- Printf.ksprintf anomaly ("Module %s is already defined")
+ Printf.ksprintf anomaly ("Module %s is already defined.")
(ModPath.to_string mp);
let new_mods = MPmap.add mp mb env.env_globals.env_modules in
let new_globals =
@@ -221,7 +221,7 @@ let shallow_add_module mp mb env =
let shallow_remove_module mp env =
if not (MPmap.mem mp env.env_globals.env_modules) then
- Printf.ksprintf anomaly ("Module %s is unknown")
+ Printf.ksprintf anomaly ("Module %s is unknown.")
(ModPath.to_string mp);
let new_mods = MPmap.remove mp env.env_globals.env_modules in
let new_globals =
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 27f79e7963..6c38f38e29 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -100,7 +100,7 @@ let rec sorts_of_constr_args env t =
let env1 = push_rel (LocalDef (name,def,ty)) env in
sorts_of_constr_args env1 c
| _ when is_constructor_head t -> []
- | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor")
+ | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor.")
(* Prop and Set are small *)
@@ -302,11 +302,11 @@ let failwith_non_pos n ntypes c =
let failwith_non_pos_vect n ntypes v =
Array.iter (failwith_non_pos n ntypes) v;
- anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur")
+ anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur.")
let failwith_non_pos_list n ntypes l =
List.iter (failwith_non_pos n ntypes) l;
- anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur")
+ anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur.")
(* Conclusion of constructors: check the inductive type is called with
the expected parameters *)
@@ -530,18 +530,18 @@ let check_positivity env_ar mind params nrecp inds =
let check_inductive env kn mib =
Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn);
(* check mind_constraints: should be consistent with env *)
- let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in
+ let env = Environ.push_context (Univ.instantiate_univ_context mib.mind_universes) env in
(* check mind_record : TODO ? check #constructor = 1 ? *)
(* check mind_finite : always OK *)
(* check mind_ntypes *)
if Array.length mib.mind_packets <> mib.mind_ntypes then
- error "not the right number of packets";
+ user_err Pp.(str "not the right number of packets");
(* check mind_params_ctxt *)
let params = mib.mind_params_ctxt in
let _ = check_ctxt env params in
(* check mind_nparams *)
if rel_context_nhyps params <> mib.mind_nparams then
- error "number the right number of parameters";
+ user_err Pp.(str "number the right number of parameters");
(* mind_packets *)
(* - check arities *)
let env_ar = typecheck_arity env params mib.mind_packets in
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 8f23a38afc..f890adba9a 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -27,7 +27,7 @@ type mind_specif = mutual_inductive_body * one_inductive_body
let lookup_mind_specif env (kn,tyi) =
let mib = lookup_mind kn env in
if tyi >= Array.length mib.mind_packets then
- error "Inductive.lookup_mind_specif: invalid inductive index";
+ user_err Pp.(str "Inductive.lookup_mind_specif: invalid inductive index");
(mib, mib.mind_packets.(tyi))
let find_rectype env c =
@@ -75,7 +75,7 @@ let constructor_instantiate mind u mib c =
let instantiate_params full t u args sign =
let fail () =
- anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
+ anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch.") in
let (rem_args, subs, ty) =
fold_rel_context
(fun decl (largs,subs,ty) ->
@@ -232,7 +232,7 @@ let type_of_constructor_subst cstr u (mib,mip) =
let specif = mip.mind_user_lc in
let i = index_of_constructor cstr in
let nconstr = Array.length mip.mind_consnames in
- if i > nconstr then error "Not enough constructors in the type.";
+ if i > nconstr then user_err Pp.(str "Not enough constructors in the type.");
constructor_instantiate (fst ind) u mib specif.(i-1)
let type_of_constructor_gen (cstr,u) (mib,mip as mspec) =
@@ -986,7 +986,7 @@ let check_one_fix renv recpos trees def =
List.iter (check_rec_call renv []) l;
check_rec_call renv [] c
- | Var _ -> anomaly (Pp.str "Section variable in Coqchk !")
+ | Var _ -> anomaly (Pp.str "Section variable in Coqchk!")
| Sort _ -> assert (l = [])
@@ -1004,7 +1004,7 @@ let check_one_fix renv recpos trees def =
check_rec_call renv [] a;
let renv' = push_var_renv renv (x,a) in
check_nested_fix_body renv' (decr-1) recArgsDecrArg b
- | _ -> anomaly (Pp.str "Not enough abstractions in fix body")
+ | _ -> anomaly (Pp.str "Not enough abstractions in fix body.")
in
check_rec_call renv [] def
@@ -1018,7 +1018,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
|| Array.length names <> nbfix
|| bodynum < 0
|| bodynum >= nbfix
- then anomaly (Pp.str "Ill-formed fix term");
+ then anomaly (Pp.str "Ill-formed fix term.");
let fixenv = push_rec_types recdef env in
let raise_err env i err =
error_ill_formed_rec_body env err names i in
@@ -1039,7 +1039,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
raise_err env i (RecursionNotOnInductiveType a) in
(mind, (env', b))
else check_occur env' (n+1) b
- else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call")
+ else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.")
| _ -> raise_err env i NotEnoughAbstractionInFixBody in
check_occur fixenv 1 def in
(* Do it on every fixpoint *)
@@ -1073,7 +1073,7 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
exception CoFixGuardError of env * guard_error
let anomaly_ill_typed () =
- anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor")
+ anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor.")
let rec codomain_is_coind env c =
let b = whd_all env c in
diff --git a/checker/modops.ml b/checker/modops.ml
index 07dda8a06d..bed31143bf 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -16,21 +16,21 @@ open Declarations
(*i*)
let error_not_a_constant l =
- error ("\""^(Label.to_string l)^"\" is not a constant")
+ user_err Pp.(str ("\""^(Label.to_string l)^"\" is not a constant"))
-let error_not_a_functor () = error "Application of not a functor"
+let error_not_a_functor () = user_err Pp.(str "Application of not a functor")
-let error_incompatible_modtypes _ _ = error "Incompatible module types"
+let error_incompatible_modtypes _ _ = user_err Pp.(str "Incompatible module types")
let error_not_match l _ =
- error ("Signature components for label "^Label.to_string l^" do not match")
+ user_err Pp.(str ("Signature components for label "^Label.to_string l^" do not match"))
-let error_no_such_label l = error ("No such label "^Label.to_string l)
+let error_no_such_label l = user_err Pp.(str ("No such label "^Label.to_string l))
let error_no_such_label_sub l l1 =
let l1 = ModPath.to_string l1 in
- error ("The field "^
- Label.to_string l^" is missing in "^l1^".")
+ user_err Pp.(str ("The field "^
+ Label.to_string l^" is missing in "^l1^"."))
let error_not_a_module_loc ?loc s =
user_err ?loc (str ("\""^Label.to_string s^"\" is not a module"))
@@ -38,7 +38,7 @@ let error_not_a_module_loc ?loc s =
let error_not_a_module s = error_not_a_module_loc s
let error_with_module () =
- error "Unsupported 'with' constraint in module implementation"
+ user_err Pp.(str "Unsupported 'with' constraint in module implementation")
let is_functor = function
| MoreFunctor _ -> true
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 28c0126b41..ba0b017844 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -333,13 +333,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
(* Eta-expansion on the fly *)
| (FLambda _, _) ->
if v1 <> [] then
- anomaly (Pp.str "conversion was given unreduced term (FLambda)");
+ anomaly (Pp.str "conversion was given unreduced term (FLambda).");
let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
eqappr univ CONV infos
(el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2))
| (_, FLambda _) ->
if v2 <> [] then
- anomaly (Pp.str "conversion was given unreduced term (FLambda)");
+ anomaly (Pp.str "conversion was given unreduced term (FLambda).");
let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
eqappr univ CONV infos
(el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[]))
@@ -479,7 +479,7 @@ let vm_conv cv_pb = fconv cv_pb true
let hnf_prod_app env t n =
match whd_all env t with
| Prod (_,_,b) -> subst1 n b
- | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
+ | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.")
let hnf_prod_applist env t nl =
List.fold_left (hnf_prod_app env) t nl
@@ -536,5 +536,5 @@ let dest_arity env c =
let l, c = dest_prod_assum env c in
match c with
| Sort s -> l,s
- | _ -> error "not an arity"
+ | _ -> user_err Pp.(str "not an arity")
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 53d80c6d55..c70cd5c8ce 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -40,7 +40,7 @@ let check_engagement env expected_impredicative_set =
begin
match impredicative_set, expected_impredicative_set with
| PredicativeSet, ImpredicativeSet ->
- CErrors.error "Needs option -impredicative-set."
+ CErrors.user_err Pp.(str "Needs option -impredicative-set.")
| _ -> ()
end;
()
@@ -61,7 +61,7 @@ let check_imports f caller env needed =
let actual_stamp = lookup_digest env dp in
if stamp <> actual_stamp then report_clash f caller dp
with Not_found ->
- error ("Reference to unknown module " ^ (DirPath.to_string dp))
+ user_err Pp.(str ("Reference to unknown module " ^ (DirPath.to_string dp)))
in
Array.iter check needed
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index a290b240d8..2d04b77e46 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -302,22 +302,22 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
let c2 = force_constr lc2 in
check_conv conv env c1 c2))
| IndType ((kn,i),mind1) ->
- ignore (CErrors.error (
+ ignore (CErrors.user_err (Pp.str (
"The kernel does not recognize yet that a parameter can be " ^
"instantiated by an inductive type. Hint: you can rename the " ^
"inductive type and give a definition to map the old name to the new " ^
- "name."));
+ "name.")));
if constant_has_body cb2 then error () ;
let u = inductive_instance mind1 in
let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in
let typ2 = Typeops.type_of_constant_type env cb2.const_type in
check_conv conv_leq env arity1 typ2
| IndConstr (((kn,i),j) as cstr,mind1) ->
- ignore (CErrors.error (
+ ignore (CErrors.user_err (Pp.str (
"The kernel does not recognize yet that a parameter can be " ^
"instantiated by a constructor. Hint: you can rename the " ^
"constructor and give a definition to map the old name to the new " ^
- "name."));
+ "name.")));
if constant_has_body cb2 then error () ;
let u1 = inductive_instance mind1 in
let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
diff --git a/checker/term.ml b/checker/term.ml
index 24e6008d34..75c566aeb7 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -273,14 +273,14 @@ let decompose_lam =
abstractions *)
let decompose_lam_n_assum n =
if n < 0 then
- error "decompose_lam_n_assum: integer parameter must be positive";
+ user_err Pp.(str "decompose_lam_n_assum: integer parameter must be positive");
let rec lamdec_rec l n c =
if Int.equal n 0 then l,c
else match c with
| Lambda (x,t,c) -> lamdec_rec (LocalAssum (x,t) :: l) (n-1) c
| LetIn (x,b,t,c) -> lamdec_rec (LocalDef (x,b,t) :: l) n c
| Cast (c,_,_) -> lamdec_rec l n c
- | c -> error "decompose_lam_n_assum: not enough abstractions"
+ | c -> user_err Pp.(str "decompose_lam_n_assum: not enough abstractions")
in
lamdec_rec empty_rel_context n
@@ -306,14 +306,14 @@ let decompose_prod_assum =
let decompose_prod_n_assum n =
if n < 0 then
- error "decompose_prod_n_assum: integer parameter must be positive";
+ user_err Pp.(str "decompose_prod_n_assum: integer parameter must be positive");
let rec prodec_rec l n c =
if Int.equal n 0 then l,c
else match c with
| Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) (n-1) c
| LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) (n-1) c
| Cast (c,_,_) -> prodec_rec l n c
- | c -> error "decompose_prod_n_assum: not enough assumptions"
+ | c -> user_err Pp.(str "decompose_prod_n_assum: not enough assumptions")
in
prodec_rec empty_rel_context n
@@ -333,7 +333,7 @@ let destArity =
| LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t)::l) c
| Cast (c,_,_) -> prodec_rec l c
| Sort s -> l,s
- | _ -> anomaly ~label:"destArity" (Pp.str "not an arity")
+ | _ -> anomaly ~label:"destArity" (Pp.str "not an arity.")
in
prodec_rec []
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 1396d56df3..0163db3347 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -262,7 +262,7 @@ let rec execute env cstr =
| Rel n -> judge_of_relative env n
- | Var _ -> anomaly (Pp.str "Section variable in Coqchk !")
+ | Var _ -> anomaly (Pp.str "Section variable in Coqchk!")
| Const c -> judge_of_constant env c
@@ -344,10 +344,10 @@ let rec execute env cstr =
(* Partial proofs: unsupported by the kernel *)
| Meta _ ->
- anomaly (Pp.str "the kernel does not support metavariables")
+ anomaly (Pp.str "the kernel does not support metavariables.")
| Evar _ ->
- anomaly (Pp.str "the kernel does not support existential variables")
+ anomaly (Pp.str "the kernel does not support existential variables.")
and execute_type env constr =
let j = execute env constr in
diff --git a/checker/univ.ml b/checker/univ.ml
index fb1a0faa78..5717432315 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -545,7 +545,7 @@ let repr g u =
let a =
try UMap.find u g
with Not_found -> anomaly ~label:"Univ.repr"
- (str"Universe " ++ Level.pr u ++ str" undefined")
+ (str"Universe " ++ Level.pr u ++ str" undefined.")
in
match a with
| Equiv v -> repr_rec v
@@ -848,7 +848,7 @@ let merge g arcu arcv =
else (max_rank, old_max_rank, best_arc, arc::rest)
in
match between g arcu arcv with
- | [] -> anomaly (str "Univ.between")
+ | [] -> anomaly (str "Univ.between.")
| arc::rest ->
let (max_rank, old_max_rank, best_arc, rest) =
List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in
@@ -911,7 +911,7 @@ let enforce_univ_eq u v g =
| FastLT -> error_inconsistency Eq u v
| FastLE -> merge g arcv arcu
| FastNLE -> merge_disc g arcu arcv
- | FastEQ -> anomaly (Pp.str "Univ.compare"))
+ | FastEQ -> anomaly (Pp.str "Univ.compare."))
(* enforce_univ_leq : Level.t -> Level.t -> unit *)
(* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
@@ -924,7 +924,7 @@ let enforce_univ_leq u v g =
| FastLT -> error_inconsistency Le u v
| FastLE -> merge g arcv arcu
| FastNLE -> fst (setleq g arcu arcv)
- | FastEQ -> anomaly (Pp.str "Univ.compare")
+ | FastEQ -> anomaly (Pp.str "Univ.compare.")
(* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
let enforce_univ_lt u v g =
@@ -937,7 +937,7 @@ let enforce_univ_lt u v g =
| FastNLE ->
match fast_compare_neq false g arcv arcu with
FastNLE -> fst (setlt g arcu arcv)
- | FastEQ -> anomaly (Pp.str "Univ.compare")
+ | FastEQ -> anomaly (Pp.str "Univ.compare.")
| FastLE | FastLT -> error_inconsistency Lt u v
(* Prop = Set is forbidden here. *)
@@ -995,13 +995,13 @@ let constraint_add_leq v u c =
else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
if Level.equal x y then (* u+(k+1) <= u *)
raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u))
- else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints")
+ else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.")
else if j = 0 then
Constraint.add (x,Le,y) c
else (* j >= 1 *) (* m = n + k, u <= v+k *)
if Level.equal x y then c (* u <= u+k, trivial *)
else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
- else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints")
+ else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints.")
let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
@@ -1012,7 +1012,7 @@ let enforce_leq u v c =
match v with
| Universe.Huniv.Cons (v, _, Universe.Huniv.Nil) ->
Universe.Huniv.fold (fun u -> constraint_add_leq u v) u c
- | _ -> anomaly (Pp.str"A universe bound can only be a variable")
+ | _ -> anomaly (Pp.str"A universe bound can only be a variable.")
let enforce_leq u v c =
if check_univ_leq u v then c
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 04:01:02 +0000