diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-28 21:05:35 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-28 21:05:35 +0000 |
| commit | 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 (patch) | |
| tree | e035f490e2c748356df73342876b22cfcb3bc5a0 /checker/inductive.ml | |
| parent | 5e8824960f68f529869ac299b030282cc916ba2c (diff) | |
Uniformization of the "anomaly" command.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/inductive.ml')
| -rw-r--r-- | checker/inductive.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index b04c77ad8..abc162af7 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -67,7 +67,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) = fold_rel_context (fun (_,copt,_) (largs,subs,ty) -> @@ -778,7 +778,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 @@ -792,7 +792,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = or Array.length names <> nbfix or bodynum < 0 or 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 raise_err env i err = error_ill_formed_rec_body env err names i in @@ -813,7 +813,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 *) @@ -842,7 +842,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 |