Uniformization of the "anomaly" command.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7

17 files changed, 75 insertions, 74 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 1630cff38b..b22dd42e7b 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -797,7 +797,7 @@ let rec drop_parameters depth n argstk =
     | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *)
 	if Int.equal n 0 then []
 	else anomaly
-	  "ill-typed term: found a match on a partially applied constructor"
+	  (Pp.str "ill-typed term: found a match on a partially applied constructor")
     | _ -> assert false
 	(* strip_update_shift_app only produces Zapp and Zshift items *)
 
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 6c22db3a2c..4fde7474b5 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -26,7 +26,7 @@ open Environ
 type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
 
 let pop_dirpath p = match Dir_path.repr p with
-  | [] -> anomaly "dirpath_prefix: empty dirpath"
+  | [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath")
   | _::l -> Dir_path.make l
 
 let pop_mind kn =
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 27b7c76b4c..a36e2dcf66 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -460,13 +460,13 @@ fun env field value ->
     match value with
       | Const kn ->  retroknowledge add_int31_op env value 2
 	                               op kn
-      | _ -> anomaly "Environ.register: should be a constant"
+      | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")
   in
   let add_int31_unop_from_const op =
     match value with
       | Const kn ->  retroknowledge add_int31_op env value 1
 	                               op kn
-      | _ -> anomaly "Environ.register: should be a constant"
+      | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")
   in
   (* subfunction which completes the function constr_of_int31 above
      by performing the actual retroknowledge operations *)
@@ -481,9 +481,9 @@ fun env field value ->
 		  | Ind i31t ->
 		      Retroknowledge.add_vm_decompile_constant_info rk
 		               value (constr_of_int31 i31t i31bit_type)
-		  | _ -> anomaly "Environ.register: should be an inductive type")
-	    | _ -> anomaly "Environ.register: Int31Bits should be an inductive type")
-      | _ -> anomaly "Environ.register: add_int31_decompilation_from_type called with an abnormal field"
+		  | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type"))
+	    | _ -> anomaly ~label:"Environ.register" (Pp.str "Int31Bits should be an inductive type"))
+      | _ -> anomaly ~label:"Environ.register" (Pp.str "add_int31_decompilation_from_type called with an abnormal field")
   in
   {env with retroknowledge =
   let retroknowledge_with_reactive_info =
@@ -491,7 +491,7 @@ fun env field value ->
     | KInt31 (_, Int31Type) ->
         let i31c = match value with
                      | Ind i31t -> (Construct (i31t, 1))
-		     | _ -> anomaly "Environ.register: should be an inductive type"
+		     | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type")
 	in
 	add_int31_decompilation_from_type
 	  (add_vm_before_match_info
@@ -511,14 +511,14 @@ fun env field value ->
 				 | Const kn ->
 				     retroknowledge add_int31_op env value 3
 	                               Cbytecodes.Kdiv21int31 kn
-				 | _ -> anomaly "Environ.register: should be a constant")
+				 | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant"))
     | KInt31 (_, Int31Div) -> add_int31_binop_from_const Cbytecodes.Kdivint31
     | KInt31 (_, Int31AddMulDiv) -> (* this is a ternary operation *)
                                 (match value with
 				 | Const kn ->
 				     retroknowledge add_int31_op env value 3
 	                               Cbytecodes.Kaddmuldivint31 kn
-				 | _ -> anomaly "Environ.register: should be a constant")
+				 | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant"))
     | KInt31 (_, Int31Compare) -> add_int31_binop_from_const Cbytecodes.Kcompareint31
     | KInt31 (_, Int31Head0) -> add_int31_unop_from_const Cbytecodes.Khead0int31
     | KInt31 (_, Int31Tail0) -> add_int31_unop_from_const Cbytecodes.Ktail0int31
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 165af63cff..357a48080c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -180,7 +180,7 @@ let infer_constructor_packet env_ar_par params lc =
    conditions. *)
 let typecheck_inductive env mie =
   let () = match mie.mind_entry_inds with
-  | [] -> anomaly "empty inductive types declaration"
+  | [] -> anomaly (Pp.str "empty inductive types declaration")
   | _ -> ()
   in
   (* Check unicity of names *)
@@ -327,11 +327,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 "failwith_non_pos_vect: 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 "failwith_non_pos_list: 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")
 
 (* Check the inductive type is called with the expected parameters *)
 let check_correct_par (env,n,ntypes,_) hyps l largs =
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 740ac8c13d..31d9f48ac4 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
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 0d29cf10b6..b566dd8afa 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -229,7 +229,7 @@ and check_with_mod env sign (idl,mp1) mp equiv =
 and translate_module env mp inl me =
   match me.mod_entry_expr, me.mod_entry_type with
     | None, None ->
-	anomaly "Mod_typing.translate_module: empty type and expr in module entry"
+	anomaly ~label:"Mod_typing.translate_module" (Pp.str "empty type and expr in module entry")
     | None, Some mte ->
 	let mtb = translate_module_type env mp inl mte in
 	  { mod_mp = mp;
diff --git a/kernel/modops.ml b/kernel/modops.ml
index e135866899..e247a57121 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -244,7 +244,7 @@ let add_retroknowledge mp =
 	  (match e with 
 	    | Const kn -> kind_of_term (mkConst kn)
 	    | Ind ind -> kind_of_term (mkInd ind)
-	    | _ -> anomaly "Modops.add_retroknowledge: had to import an unsupported kind of term")
+	    | _ -> anomaly ~label:"Modops.add_retroknowledge" (Pp.str "had to import an unsupported kind of term"))
   in
   fun lclrk env ->
   (* The order of the declaration matters, for instance (and it's at the
@@ -278,7 +278,7 @@ and add_module mb env =
 	  add_retroknowledge mp mb.mod_retroknowledge 
 	    (add_signature mp sign mb.mod_delta env)
       | SEBfunctor _ -> env
-      | _ -> anomaly "Modops:the evaluation of the structure failed "
+      | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
 
 let strengthen_const mp_from l cb resolver =
   match cb.const_body with
@@ -308,7 +308,7 @@ let rec strengthen_mod mp_from mp_to mb =
 	       (add_delta_resolver mb.mod_delta resolve_out);
 	       mod_retroknowledge = mb.mod_retroknowledge}
      | SEBfunctor _ -> mb
-     | _ -> anomaly "Modops:the evaluation of the structure failed "
+     | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
 
 and strengthen_sig mp_from sign mp_to resolver =
   match sign with
@@ -345,7 +345,7 @@ let strengthen mtb mp =
 	       typ_delta = add_delta_resolver mtb.typ_delta
 		(add_mp_delta_resolver mtb.typ_mp mp resolve_out)}
       | SEBfunctor _ -> mtb
-      | _ -> anomaly "Modops:the evaluation of the structure failed "
+      | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
 
 let module_type_of_module mp mb =
   match mp with
@@ -408,7 +408,7 @@ let rec strengthen_and_subst_mod
 	   subst_module subst 
 	     (fun resolver subst-> subst_dom_codom_delta_resolver subst resolver) mb  
 	
-       | _ -> anomaly "Modops:the evaluation of the structure failed "
+       | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
 	   
 and strengthen_and_subst_struct 
     str subst mp_alias mp_from mp_to alias incl resolver =
@@ -518,7 +518,7 @@ let strengthen_and_subst_mb mb mp include_b =
 	  let subst = map_mp mb.mod_mp mp empty_delta_resolver in
 	  subst_module subst 
 	    (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mb 
-      | _ -> anomaly "Modops:the evaluation of the structure failed "
+      | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
 
 
 let subst_modtype_and_resolver mtb mp =
@@ -572,7 +572,7 @@ let rec collect_mbid l = function
   | SEBstruct str as s->
       let str_clean = Util.List.smartmap (clean_struct l) str in 
 	if  str_clean == str then s else SEBstruct(str_clean)
-  |  _ -> anomaly "Modops:the evaluation of the structure failed "
+  |  _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
        
        
 let clean_bounded_mod_expr = function
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 4e78d2bd43..6b92474769 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -112,32 +112,32 @@ type symbol =
 let get_value tbl i =
   match tbl.(i) with
     | SymbValue v -> v
-    | _ -> anomaly "get_value failed"
+    | _ -> anomaly (Pp.str "get_value failed")
 
 let get_sort tbl i =
   match tbl.(i) with
     | SymbSort s -> s
-    | _ -> anomaly "get_sort failed"
+    | _ -> anomaly (Pp.str "get_sort failed")
 
 let get_name tbl i =
   match tbl.(i) with
     | SymbName id -> id
-    | _ -> anomaly "get_name failed"
+    | _ -> anomaly (Pp.str "get_name failed")
 
 let get_const tbl i =
   match tbl.(i) with
     | SymbConst kn -> kn
-    | _ -> anomaly "get_const failed"
+    | _ -> anomaly (Pp.str "get_const failed")
 
 let get_match tbl i =
   match tbl.(i) with
     | SymbMatch case_info -> case_info
-    | _ -> anomaly "get_match failed"
+    | _ -> anomaly (Pp.str "get_match failed")
 
 let get_ind tbl i =
   match tbl.(i) with
     | SymbInd ind -> ind
-    | _ -> anomaly "get_ind failed"
+    | _ -> anomaly (Pp.str "get_ind failed")
 
 let symbols_list = ref ([] : symbol list)
 
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 4ba3056600..1c931ab85e 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -148,6 +148,6 @@ let native_conv pb env t1 t2 =
         (* TODO change 0 when we can have deBruijn *)
         conv_val pb 0 !rt1 !rt2 empty_constraint
       end
-  | _ -> anomaly "Compilation failure" 
+  | _ -> anomaly (Pp.str "Compilation failure") 
 
 let _ = set_nat_conv native_conv
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 86fe45bdc4..09202f6a7c 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -19,7 +19,7 @@ open Envars
 used by the native compiler. *)
 
 let get_load_paths =
-  ref (fun _ -> anomaly "get_load_paths not initialized" : unit -> string list)
+  ref (fun _ -> anomaly (Pp.str "get_load_paths not initialized") : unit -> string list)
 
 let open_header = ["Nativevalues";
                    "Nativecode";
@@ -85,7 +85,7 @@ let call_linker ~fatal prefix f upds =
     register_native_file prefix
    with | Dynlink.Error e ->
           let msg = "Dynlink error, " ^ Dynlink.error_message e in
-          if fatal then anomaly msg else Pp.msg_warning (Pp.str msg)
+          if fatal then anomaly (Pp.str msg) else Pp.msg_warning (Pp.str msg)
         | _ -> let msg = "Dynlink error" in
-          if fatal then anomaly msg else Pp.msg_warning (Pp.str msg));
+          if fatal then anomaly (Pp.str msg) else Pp.msg_warning (Pp.str msg));
   match upds with Some upds -> update_locations upds | _ -> ()
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index fc4255aaf8..2f317ca969 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -195,7 +195,8 @@ let mk_block tag args =
 
 (* Two instances of dummy_value should not be pointer equal, otherwise
  comparing them as terms would succeed *)
-let dummy_value : unit -> t = fun () _ -> anomaly "Evaluation failed"
+let dummy_value : unit -> t =
+  fun () _ -> anomaly ~label:"native" (Pp.str "Evaluation failed")
 
 let cast_accu v = (Obj.magic v:accumulator)
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 6a72487495..7a14e57cc2 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -133,7 +133,7 @@ let betazeta_appvect n c v =
     match kind_of_term t, stack with
         Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
       | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack
-      | _ -> anomaly "Not enough lambda/let's" in
+      | _ -> anomaly (Pp.str "Not enough lambda/let's") in
   stacklam n [] c (Array.to_list v)
 
 (********************************************************************)
@@ -267,7 +267,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	(match kind_of_term a1, kind_of_term a2 with
 	   | (Sort s1, Sort s2) ->
 	       if not (is_empty_stack v1 && is_empty_stack v2) then
-		 anomaly "conversion was given ill-typed terms (Sort)";
+		 anomaly (Pp.str "conversion was given ill-typed terms (Sort)");
 	       sort_cmp cv_pb s1 s2 cuniv
 	   | (Meta n, Meta m) ->
                if Int.equal n m
@@ -318,7 +318,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         (* Inconsistency: we tolerate that v1, v2 contain shift and update but
            we throw them away *)
         if not (is_empty_stack v1 && is_empty_stack v2) then
-	  anomaly "conversion was given ill-typed terms (FLambda)";
+	  anomaly (Pp.str "conversion was given ill-typed terms (FLambda)");
         let (_,ty1,bd1) = destFLambda mk_clos hd1 in
         let (_,ty2,bd2) = destFLambda mk_clos hd2 in
         let u1 = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
@@ -326,7 +326,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 
     | (FProd (_,c1,c2), FProd (_,c'1,c'2)) ->
         if not (is_empty_stack v1 && is_empty_stack v2) then
-	  anomaly "conversion was given ill-typed terms (FProd)";
+	  anomaly (Pp.str "conversion was given ill-typed terms (FProd)");
 	(* Luo's system *)
         let u1 = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in
         ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 u1
@@ -336,7 +336,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         let () = match v1 with
         | [] -> ()
         | _ ->
-          anomaly "conversion was given unreduced term (FLambda)"
+          anomaly (Pp.str "conversion was given unreduced term (FLambda)")
         in
         let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
 	eqappr CONV l2r infos
@@ -345,7 +345,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         let () = match v2 with
         | [] -> ()
         | _ ->
-	  anomaly "conversion was given unreduced term (FLambda)"
+	  anomaly (Pp.str "conversion was given unreduced term (FLambda)")
 	in
         let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
 	eqappr CONV l2r infos
@@ -520,7 +520,7 @@ let conv env t1 t2 =
 let hnf_prod_app env t n =
   match kind_of_term (whd_betadeltaiota env t) with
     | Prod (_,_,b) -> subst1 n b
-    | _ -> anomaly "hnf_prod_app: 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
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a8c850ecde..2e21a86ff8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -286,14 +286,14 @@ let add_constant dir l decl senv =
 let add_mind dir l mie senv =
   let () = match mie.mind_entry_inds with
   | [] ->
-    anomaly "empty inductive types declaration"
+    anomaly (Pp.str "empty inductive types declaration")
             (* this test is repeated by translate_mind *)
   | _ -> ()
   in
   let id = (List.nth mie.mind_entry_inds 0).mind_entry_typename in
   if not (Label.equal l (Label.of_id id)) then
-    anomaly ("the label of inductive packet and its first inductive"^
-	     " type do not match");
+    anomaly (Pp.str "the label of inductive packet and its first inductive \
+	     type do not match");
   let kn = make_mind senv.modinfo.modpath dir l in
   let mib = translate_mind senv.env kn mie in
   let mib = match mib.mind_hyps with [] -> hcons_mind mib | _ -> mib in
@@ -499,7 +499,7 @@ let end_module l restype senv =
 let add_module_parameter mbid mte inl senv =
   let () = match senv.revstruct, senv.loads with
   | [], _ :: _ | _ :: _, [] ->
-    anomaly "Cannot add a module parameter to a non empty module"
+    anomaly (Pp.str "Cannot add a module parameter to a non empty module")
   | _ -> ()
   in
   let mtb = translate_module_type senv.env (MPbound mbid) inl mte in
@@ -510,7 +510,7 @@ let add_module_parameter mbid mte inl senv =
     | STRUCT params -> STRUCT ((mbid,mtb) :: params)
     | SIG params -> SIG ((mbid,mtb) :: params)
     | _ ->
-	anomaly "Module parameters can only be added to modules or signatures"  
+	anomaly (Pp.str "Module parameters can only be added to modules or signatures")  
   in
     
   let resolver_of_param = match mtb.typ_expr with
@@ -644,10 +644,10 @@ let is_empty senv = match senv.revstruct, senv.modinfo.variant with
 
 let start_library dir senv =
   if not (is_empty senv) then
-    anomaly "Safe_typing.start_library: environment should be empty";
+    anomaly ~label:"Safe_typing.start_library" (Pp.str "environment should be empty");
   let dir_path,l =
     match (Dir_path.repr dir) with
-	[] -> anomaly "Empty dirpath in Safe_typing.start_library"
+	[] -> anomaly (Pp.str "Empty dirpath in Safe_typing.start_library")
       | hd::tl ->
 	  Dir_path.make tl, Label.of_id hd
   in
@@ -686,9 +686,9 @@ let export senv dir =
     match modinfo.variant with
       | LIBRARY dp ->
 	  if not (Dir_path.equal dir dp) then
-	    anomaly "We are not exporting the right library!"
+	    anomaly (Pp.str "We are not exporting the right library!")
       | _ ->
-	  anomaly "We are not exporting the library"
+	  anomaly (Pp.str "We are not exporting the library")
   end;
   (*if senv.modinfo.params <> [] || senv.modinfo.restype <> None then
     (* error_export_simple *) (); *)
diff --git a/kernel/term.ml b/kernel/term.ml
index e4657ce28c..93e870015e 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -407,7 +407,7 @@ let isConstruct c = match kind_of_term c with Construct _ -> true | _ -> false
 (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
 let destCase c = match kind_of_term c with
   | Case (ci,p,c,v) -> (ci,p,c,v)
-  | _ -> anomaly "destCase"
+  | _ -> invalid_arg "destCase"
 
 let isCase c =  match kind_of_term c with Case _ -> true | _ -> false
 
@@ -1160,7 +1160,7 @@ let destArity =
     | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c
     | Cast (c,_,_)      -> prodec_rec l c
     | Sort s          -> l,s
-    | _               -> anomaly "destArity: not an arity"
+    | _               -> anomaly ~label:"destArity" (Pp.str "not an arity")
   in
   prodec_rec []
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index e611682002..efc7a4ee8b 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -466,10 +466,10 @@ let rec execute env cstr cu =
 
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
-	anomaly "the kernel does not support metavariables"
+	anomaly (Pp.str "the kernel does not support metavariables")
 
     | Evar _ ->
-	anomaly "the kernel does not support existential variables"
+	anomaly (Pp.str "the kernel does not support existential variables")
 
 and execute_type env constr cu =
   let (j,cu1) = execute env constr cu in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 71b417624d..cfb7049323 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -143,8 +143,8 @@ let super = function
   | Atom u ->
       Max ([],[u])
   | Max _ ->
-      anomaly ("Cannot take the successor of a non variable universe:\n"^
-               "(maybe a bugged tactic)")
+      anomaly (str "Cannot take the successor of a non variable universe" ++ spc () ++
+               str "(maybe a bugged tactic)")
 
 (* Returns the formal universe that is greater than the universes u and v.
    Used to type the products. *)
@@ -224,8 +224,8 @@ let repr g u =
   let rec repr_rec u =
     let a =
       try UniverseLMap.find u g
-      with Not_found -> anomalylabstrm "Univ.repr"
-	  (str"Universe " ++ pr_uni_level u ++ str" undefined")
+      with Not_found -> anomaly ~label:"Univ.repr"
+	  (str "Universe" ++ spc () ++ pr_uni_level u ++ spc () ++ str "undefined")
     in
     match a with
       | Equiv v -> repr_rec v
@@ -432,7 +432,7 @@ let check_eq g u v =
         (* TODO: remove elements of lt in le! *)
         compare_list (check_equal g) ule vle &&
         compare_list (check_equal g) ult vlt
-    | _ -> anomaly "check_eq" (* not complete! (Atom(u) = Max([u],[]) *)
+    | _ -> anomaly (str "check_eq") (* not complete! (Atom(u) = Max([u],[]) *)
 
 let check_leq g u v =
   match u,v with
@@ -440,7 +440,7 @@ let check_leq g u v =
     | Max(le,lt), Atom vl ->
         List.for_all (fun ul -> check_smaller g false ul vl) le &&
         List.for_all (fun ul -> check_smaller g true ul vl) lt
-    | _ -> anomaly "check_leq"
+    | _ -> anomaly (str "check_leq")
 
 (** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *)
 
@@ -483,7 +483,7 @@ let merge g arcu arcv =
       else (max_rank, old_max_rank, best_arc, arc::rest)
     in
     match between g arcu arcv with
-      | [] -> anomaly "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
@@ -540,7 +540,7 @@ let enforce_univ_leq u v g =
     | LT p -> error_inconsistency Le u v (List.rev p)
     | LE _ -> merge g arcv arcu
     | NLE -> fst (setleq g arcu arcv)
-    | EQ -> anomaly "Univ.compare"
+    | EQ -> anomaly (Pp.str "Univ.compare")
 
 (* enforc_univ_eq : UniverseLevel.t -> UniverseLevel.t -> unit *)
 (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
@@ -556,7 +556,7 @@ let enforce_univ_eq u v g =
            | LT p -> error_inconsistency Eq u v (List.rev p)
            | LE _ -> merge g arcv arcu
            | NLE -> merge_disc g arcu arcv
-           | EQ -> anomaly "Univ.compare")
+           | EQ -> 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 =
@@ -569,7 +569,7 @@ let enforce_univ_lt u v g =
     | NLE ->
       (match compare_neq false g arcv arcu with
 	  NLE -> fst (setlt g arcu arcv)
-	| EQ -> anomaly "Univ.compare"
+	| EQ -> anomaly (Pp.str "Univ.compare")
 	| (LE p|LT p) -> error_inconsistency Lt u v (List.rev p))
 
 (* Constraints and sets of consrtaints. *)
@@ -615,14 +615,14 @@ let enforce_leq u v c =
   | Max (gel,gtl), Atom v ->
       let d = List.fold_right (fun u -> constraint_add_leq u v) gel c in
       List.fold_right (fun u -> Constraint.add (u,Lt,v)) gtl d
-  | _ -> anomaly "A universe bound can only be a variable"
+  | _ -> anomaly (Pp.str "A universe bound can only be a variable")
 
 let enforce_eq u v c =
   match (u,v) with
     | Atom u, Atom v ->
       (* We discard trivial constraints like u=u *)
       if UniverseLevel.equal u v then c else Constraint.add (u,Eq,v) c
-    | _ -> anomaly "A universe comparison can only happen between variables"
+    | _ -> anomaly (Pp.str "A universe comparison can only happen between variables")
 
 let merge_constraints c g =
   Constraint.fold enforce_constraint c g
@@ -876,7 +876,7 @@ let is_direct_sort_constraint s v = match s with
 
 let solve_constraints_system levels level_bounds =
   let levels =
-    Array.map (Option.map (function Atom u -> u | _ -> anomaly "expects Atom"))
+    Array.map (Option.map (function Atom u -> u | _ -> anomaly (Pp.str "expects Atom")))
       levels in
   let v = Array.copy level_bounds in
   let nind = Array.length v in
@@ -899,7 +899,7 @@ let subst_large_constraint u u' v =
       if is_direct_constraint u v then sup u' (remove_large_constraint u v)
       else v
   | _ ->
-      anomaly "expect a universe level"
+      anomaly (Pp.str "expect a universe level")
 
 let subst_large_constraints =
   List.fold_right (fun (u,u') -> subst_large_constraint u u')
@@ -910,7 +910,7 @@ let no_upper_constraints u cst =
     let test (u1, _, _) =
       not (Int.equal (UniverseLevel.compare u1 u) 0) in
     Constraint.for_all test cst
-  | Max _ -> anomaly "no_upper_constraints"
+  | Max _ -> anomaly (Pp.str "no_upper_constraints")
 
 (* Is u mentionned in v (or equals to v) ? *)
 
@@ -918,7 +918,7 @@ let univ_depends u v =
   match u, v with
     | Atom u, Atom v -> UniverseLevel.equal u v
     | Atom u, Max (gel,gtl) -> List.mem u gel || List.mem u gtl
-    | _ -> anomaly "univ_depends given a non-atomic 1st arg"
+    | _ -> anomaly (Pp.str "univ_depends given a non-atomic 1st arg")
 
 (* Pretty-printing *)
 
diff --git a/kernel/vm.ml b/kernel/vm.ml
index b6a39b0421..c6491c479c 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -222,7 +222,7 @@ let whd_val : values -> whd =
 	   | 1 -> Vfix(Obj.obj o, None)
 	   | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o))
 	   | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
-	   | _ -> Errors.anomaly "Vm.whd : kind_of_closure does not work")
+	   | _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work"))
 	else Vconstr_block(Obj.obj o)