diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 740ac8c13..31d9f48ac 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -63,7 +63,7 @@ let constructor_instantiate mind mib c = let instantiate_params full t args sign = let fail () = - anomaly "instantiate_params: type, ctxt and args mismatch" in + anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in let (rem_args, subs, ty) = Sign.fold_rel_context (fun (_,copt,_) (largs,subs,ty) -> @@ -777,7 +777,7 @@ let check_one_fix renv recpos 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 "Not enough abstractions in fix body" + | _ -> anomaly (Pp.str "Not enough abstractions in fix body") in check_rec_call renv [] def @@ -793,7 +793,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = || not (Int.equal (Array.length names) nbfix) || bodynum < 0 || bodynum >= nbfix - then anomaly "Ill-formed fix term"; + then anomaly (Pp.str "Ill-formed fix term"); let fixenv = push_rec_types recdef env in let vdefj = judgment_of_fixpoint recdef in let raise_err env i err = @@ -815,7 +815,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 "check_one_fix: 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 *) @@ -845,7 +845,7 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; exception CoFixGuardError of env * guard_error let anomaly_ill_typed () = - anomaly "check_one_cofix: 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_betadeltaiota env c in |