Uniformization of the "anomaly" command.

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

19 files changed, 66 insertions, 60 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index bcf4b9e4a..ce8e296ba 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
 open Errors
 open Util
 open Names
@@ -64,7 +65,7 @@ let error_needs_inversion env x t =
 
 let rec list_try_compile f = function
   | [a] -> f a
-  | [] -> anomaly "try_find_f"
+  | [] -> anomaly (str "try_find_f")
   | h::t ->
       try f h
       with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _
@@ -149,9 +150,9 @@ let feed_history arg = function
   | Continuation (n, l, h) when n>=1 ->
       Continuation (n-1, arg :: l, h)
   | Continuation (n, _, _) ->
-      anomaly ("Bad number of expected remaining patterns: "^(string_of_int n))
+      anomaly (str "Bad number of expected remaining patterns: " ++ int n)
   | Result _ ->
-      anomaly "Exhausted pattern history"
+      anomaly (Pp.str "Exhausted pattern history")
 
 (* This is for non exhaustive error message *)
 
@@ -177,7 +178,7 @@ let pop_history_pattern = function
   | Continuation (0, l, MakeConstructor (pci, rh)) ->
       feed_history (PatCstr (Loc.ghost,pci,List.rev l,Anonymous)) rh
   | _ ->
-      anomaly "Constructor not yet filled with its arguments"
+      anomaly (Pp.str "Constructor not yet filled with its arguments")
 
 let pop_history h =
   feed_history (PatVar (Loc.ghost, Anonymous)) h
@@ -403,7 +404,7 @@ let lift_tomatch_type n = liftn_tomatch_type n 1
 let current_pattern eqn =
   match eqn.patterns with
     | pat::_ -> pat
-    | [] -> anomaly "Empty list of patterns"
+    | [] -> anomaly (Pp.str "Empty list of patterns")
 
 let alias_of_pat = function
   | PatVar (_,name) -> name
@@ -415,7 +416,7 @@ let remove_current_pattern eqn =
 	{ eqn with
 	    patterns = pats;
 	    alias_stack = alias_of_pat pat :: eqn.alias_stack }
-    | [] -> anomaly "Empty list of patterns"
+    | [] -> anomaly (Pp.str "Empty list of patterns")
 
 let push_current_pattern (cur,ty) eqn =
   match eqn.patterns with
@@ -424,7 +425,7 @@ let push_current_pattern (cur,ty) eqn =
 	{ eqn with
             rhs = { eqn.rhs with rhs_env = rhs_env };
 	    patterns = pats }
-    | [] -> anomaly "Empty list of patterns"
+    | [] -> anomaly (Pp.str "Empty list of patterns")
 
 let prepend_pattern tms eqn = {eqn with patterns = tms@eqn.patterns }
 
@@ -606,7 +607,7 @@ let replace_tomatch n c =
   | Pushed ((b,tm),l,na) :: rest ->
       let b = replace_term n c depth b in
       let tm = map_tomatch_type (replace_term n c depth) tm in
-      List.iter (fun i -> if Int.equal i (n + depth) then anomaly "replace_tomatch") l;
+      List.iter (fun i -> if Int.equal i (n + depth) then anomaly (Pp.str "replace_tomatch")) l;
       Pushed ((b,tm),l,na) :: replrec depth rest
   | Alias (na,b,d) :: rest ->
       (* [b] is out of replacement scope *)
@@ -835,7 +836,7 @@ let specialize_predicate_var (cur,typ,dep) tms ccl =
 (*****************************************************************************)
 let generalize_predicate (names,na) ny d tms ccl =
   let () = match na with
-  | Anonymous -> anomaly "Undetected dependency"
+  | Anonymous -> anomaly (Pp.str "Undetected dependency")
   | _ -> () in
   let p = List.length names + 1 in
   let ccl = lift_predicate 1 ccl tms in
@@ -1697,7 +1698,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 		  if not (eq_ind ind ind') then
 		    user_err_loc (loc,"",str "Wrong inductive type.");
 		  if not (Int.equal nrealargs_ctxt (List.length realnal)) then
-		      anomaly "Ill-formed 'in' clause in cases";
+		      anomaly (Pp.str "Ill-formed 'in' clause in cases");
 		  List.rev realnal
 	      | None -> List.make nrealargs_ctxt Anonymous in
 	  (na,None,build_dependent_inductive env0 indf')
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index b398a5693..f933bf1d3 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -42,7 +42,7 @@ let apply_coercion_args env argl funj =
 	| Prod (_,c1,c2) ->
 	    (* Typage garanti par l'appel à app_coercion*)
 	    apply_rec (h::acc) (subst1 h c2) restl
-	| _ -> anomaly "apply_coercion_args"
+	| _ -> anomaly (Pp.str "apply_coercion_args")
   in
     apply_rec [] funj.uj_type argl
 
@@ -334,7 +334,7 @@ let apply_coercion env sigma p hj typ_cl =
 		   jres),
 	      jres.uj_type)
            (hj,typ_cl) p)
-  with _ -> anomaly "apply_coercion"
+  with _ -> anomaly (Pp.str "apply_coercion")
 
 let inh_app_fun env evd j =
   let t = whd_betadeltaiota env evd j.uj_type in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 2db867fc5..be3817d5e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -375,7 +375,7 @@ type binder_kind = BProd | BLambda | BLetIn
 (**********************************************************************)
 (* Main detyping function                                             *)
 
-let detype_anonymous = ref (fun loc n -> anomaly "detype: index to an anonymous variable")
+let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable"))
 let set_detype_anonymous f = detype_anonymous := f
 
 let rec detype (isgoal:bool) avoid env t =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2184d44d3..52ef44672 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -657,7 +657,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
       let filter = List.map2 (&&) filter filter' in
       (id,t,c,ty,evs,filter,occs) :: make_subst (ctxt',l,occsl)
   | [], [], [] -> []
-  | _ -> anomaly "Signature, instance and occurrences list do not match" in
+  | _ -> anomaly (Pp.str "Signature, instance and occurrences list do not match") in
 
   let rec set_holes evdref rhs = function
   | (id,_,c,cty,evsref,filter,occs)::subst ->
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index c2ba6d957..f4f373754 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -853,7 +853,7 @@ let make_projectable_subst aliases sigma evi args =
 		   cstrs)
 	    | _ ->
 		(rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs))
-	| _ -> anomaly "Instance does not match its signature")
+	| _ -> anomaly (Pp.str "Instance does not match its signature"))
       sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in
   (full_subst,cstr_subst)
 
@@ -862,7 +862,7 @@ let make_pure_subst evi args =
     (fun (id,b,c) (args,l) ->
       match args with
 	| a::rest -> (rest, (id,a)::l)
-	| _ -> anomaly "Instance does not match its signature")
+	| _ -> anomaly (Pp.str "Instance does not match its signature"))
     (evar_filtered_context evi) (Array.rev_to_list args,[]))
 
 (*------------------------------------*
@@ -1036,7 +1036,7 @@ let rec find_projectable_vars with_evars aliases sigma y subst =
 	    | _ -> subst'
 	  end
 	| [] -> subst'
-	| _ -> anomaly "More than one non var in aliases class of evar instance"
+	| _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance")
       else
 	subst' in
   Id.Map.fold is_projectable subst []
@@ -1883,7 +1883,7 @@ let undefined_evars_of_term evd t =
 	(try match (Evd.find evd n).evar_body with
 	  | Evar_empty -> Int.Set.add n acc
 	  | Evar_defined c -> evrec acc c
-	 with Not_found -> anomaly "undefined_evars_of_term: evar not found")
+	 with Not_found -> anomaly ~label:"undefined_evars_of_term" (Pp.str "evar not found"))
       | _ -> fold_constr evrec acc c
   in
   evrec Int.Set.empty t
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 4c18aec19..a6049d0cf 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -92,7 +92,7 @@ let make_evar_instance sign args =
     | (id,_,_) :: sign, c::args when isVarId id c -> instrec (sign,args)
     | (id,_,_) :: sign, c::args -> (id,c) :: instrec (sign,args)
     | [],[] -> []
-    | [],_ | _,[] -> anomaly "Signature and its instance do not match"
+    | [],_ | _,[] -> anomaly (Pp.str "Signature and its instance do not match")
   in
     instrec (sign,args)
 
@@ -157,7 +157,7 @@ module EvarInfoMap = struct
       with Not_found -> 
 	try ExistentialMap.find evk def
 	with Not_found -> 
-	  anomaly "Evd.define: cannot define undeclared evar" in
+	  anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar") in
     let newinfo =
       { oldinfo with
 	  evar_body = Evar_defined body } in
@@ -165,7 +165,7 @@ module EvarInfoMap = struct
 	| Evar_empty ->
 	    (ExistentialMap.add evk newinfo def,ExistentialMap.remove evk undef)
 	| _ ->
-	    anomaly "Evd.define: cannot define an evar twice"
+	    anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice")
 
   let is_evar = mem
 
@@ -181,7 +181,7 @@ module EvarInfoMap = struct
     let info =
       try find sigma n
       with Not_found ->
-	anomaly ("Evar "^(string_of_existential n)^" was not declared") in
+	anomaly (str "Evar " ++ str (string_of_existential n) ++ str " was not declared") in
     let hyps = evar_filtered_context info in
       instantiate_evar hyps info.evar_concl (Array.to_list args)
 
@@ -611,7 +611,7 @@ let try_meta_fvalue evd mv =
 
 let meta_fvalue evd mv =
   try try_meta_fvalue evd mv
-  with Not_found -> anomaly "meta_fvalue: meta has no value"
+  with Not_found -> anomaly ~label:"meta_fvalue" (Pp.str "meta has no value")
 
 let meta_value evd mv =
   (fst (try_meta_fvalue evd mv)).rebus
@@ -631,14 +631,14 @@ let meta_assign mv (v,pb) evd =
   | Cltyp(na,ty) ->
       { evd with
         metas = Metamap.add mv (Clval(na,(mk_freelisted v,pb),ty)) evd.metas }
-  | _ -> anomaly "meta_assign: already defined"
+  | _ -> anomaly ~label:"meta_assign" (Pp.str "already defined")
 
 let meta_reassign mv (v,pb) evd =
   match Metamap.find mv evd.metas with
   | Clval(na,_,ty) ->
       { evd with
         metas = Metamap.add mv (Clval(na,(mk_freelisted v,pb),ty)) evd.metas }
-  | _ -> anomaly "meta_reassign: not yet defined"
+  | _ -> anomaly ~label:"meta_reassign" (Pp.str "not yet defined")
 
 (* If the meta is defined then forget its name *)
 let meta_name evd mv =
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 9c08a8bf6..60b708f5b 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -245,7 +245,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 	   process_constr (push_rel d env) (i+1) (lift 1 f)
 	     (cprest,rest))
     | [],[] -> f
-    | _,[] | [],_ -> anomaly "process_constr"
+    | _,[] | [],_ -> anomaly (Pp.str "process_constr")
 
   in
   process_constr env 0 f (List.rev cstr.cs_args, recargs)
@@ -473,7 +473,7 @@ let modify_sort_scheme sort =
 	  else
 	    mkLambda (n, t, drec (npar-1) c)
       | LetIn (n,b,t,c) -> mkLetIn (n,b,t,drec npar c)
-      | _ -> anomaly "modify_sort_scheme: wrong elimination type"
+      | _ -> anomaly ~label:"modify_sort_scheme" (Pp.str "wrong elimination type")
   in
   drec
 
@@ -492,7 +492,7 @@ let weaken_sort_scheme sort npars term =
 	    mkProd (n, t, c'), mkLambda (n, t, term')
       | LetIn (n,b,t,c) -> let c',term' = drec np c in
            mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term')
-      | _ -> anomaly "weaken_sort_scheme: wrong elimination type"
+      | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type")
   in
   drec npars
 
@@ -532,7 +532,7 @@ let build_mutual_induction_scheme env sigma = function
       in
       let _ = check_arities listdepkind in
       mis_make_indrec env sigma listdepkind mib
-  | _ -> anomaly "build_induction_scheme expects a non empty list of inductive types"
+  | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types")
 
 let build_induction_scheme env sigma ind dep kind =
   let (mib,mip) = lookup_mind_specif env ind in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index d2aaea9fa..3880dfd4e 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -206,13 +206,13 @@ let instantiate_params t args sign =
     | ((_,None,_)::ctxt,a::args) ->
 	(match kind_of_term t with
 	   | Prod(_,_,t) -> inst (a::s) t (ctxt,args)
-	   | _ -> anomaly"instantiate_params: type, ctxt and args mismatch")
+	   | _ -> anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch"))
     | ((_,(Some b),_)::ctxt,args) ->
 	(match kind_of_term t with
 	   | LetIn(_,_,_,t) -> inst ((substl s b)::s) t (ctxt,args)
-	   | _ -> anomaly"instantiate_params: type, ctxt and args mismatch")
+	   | _ -> anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch"))
     | _, [] -> substl s t
-    | _ -> anomaly"instantiate_params: type, ctxt and args mismatch"
+    | _ -> anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch")
   in inst [] t (List.rev sign,args)
 
 let get_constructor (ind,mib,mip,params) j =
@@ -248,7 +248,7 @@ let instantiate_context sign args =
   | (_,None,_)::sign, a::args -> aux (a::subst) (sign,args)
   | (_,Some b,_)::sign, args -> aux (substl subst b::subst) (sign,args)
   | [], [] -> subst
-  | _ -> anomaly "Signature/instance mismatch in inductive family"
+  | _ -> anomaly (Pp.str "Signature/instance mismatch in inductive family")
   in aux [] (List.rev sign,args)
 
 let get_arity env (ind,params) =
@@ -385,7 +385,7 @@ let is_predicate_explicitly_dep env pred arsign =
           | Name _ -> true
           end
 
-      | _ -> anomaly "Non eta-expanded dep-expanded \"match\" predicate"
+      | _ -> anomaly (Pp.str "Non eta-expanded dep-expanded \"match\" predicate")
   in
   srec env pred arsign
 
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index dfc52295d..e25312e41 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -100,7 +100,7 @@ let extract_bound_vars =
   | (n :: l, (na1, na2, _) :: stk) when Int.equal k n ->
       begin match na1, na2 with
       | Name id1, Name _ -> list_insert id1 (aux (k + 1) (l, stk))
-      | Name _, Anonymous -> anomaly "Unnamed bound variable"
+      | Name _, Anonymous -> anomaly (Pp.str "Unnamed bound variable")
       | Anonymous, _ -> raise PatternMatchingFailure
       end
   | (l, _ :: stk) -> aux (k + 1) (l, stk)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 84ad8e3dd..0ecbfdbb4 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -5,6 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+open Pp
 open Errors
 open Term
 open Environ
@@ -124,7 +125,7 @@ let type_of_sort s =
 let type_of_var env id = 
   try let (_,_,ty) = lookup_named id env in ty
   with Not_found ->
-    anomaly ("type_of_var: variable "^(string_of_id id)^" unbound")
+    anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound")
 
 let sort_of_product env domsort rangsort =
   match (domsort, rangsort) with
@@ -344,4 +345,4 @@ let native_norm env c ty =
         let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
         if !Flags.debug then Pp.msg_debug (Pp.str time_info);
         nf_val env !Nativelib.rt1 ty
-    | _ -> anomaly "Compilation failure" 
+    | _ -> anomaly (Pp.str "Compilation failure") 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index c1e91ca2f..ef0869fe6 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -108,14 +108,14 @@ let rec head_pattern_bound t =
 	-> raise BoundPattern
     (* Perhaps they were arguments, but we don't beta-reduce *)
     | PLambda _ -> raise BoundPattern
-    | PCoFix _ -> anomaly "head_pattern_bound: not a type"
+    | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type")
 
 let head_of_constr_reference c = match kind_of_term c with
   | Const sp -> ConstRef sp
   | Construct sp -> ConstructRef sp
   | Ind sp -> IndRef sp
   | Var id -> VarRef id
-  | _ -> anomaly "Not a rigid reference"
+  | _ -> anomaly (Pp.str "Not a rigid reference")
 
 let pattern_of_constr sigma t =
   let ctx = ref [] in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index fe03cae8c..bcabf1cd9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -686,7 +686,7 @@ and pretype_type valcon env evdref lvar = function
                | Sort s -> s
                | Evar ev when is_Type (existential_type sigma ev) ->
 		   evd_comb1 (define_evar_as_sort) evdref ev
-               | _ -> anomaly "Found a type constraint which is not a type"
+               | _ -> anomaly (Pp.str "Found a type constraint which is not a type")
            in
 	     { utj_val = v;
 	       utj_type = s }
diff --git a/pretyping/program.ml b/pretyping/program.ml
index d2e22f71e..43175e80c 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
 open Errors
 open Util
 open Names
@@ -16,7 +17,8 @@ let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l))
 let find_reference locstr dir s =
   let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in
   try Nametab.global_of_path sp
-  with Not_found -> anomaly (locstr^": cannot find "^(Libnames.string_of_path sp))
+  with Not_found ->
+    anomaly ~label:locstr (Pp.str "cannot find" ++ spc () ++ Libnames.pr_path sp)
 
 let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
 let coq_constant locstr dir s = Globnames.constr_of_global (coq_reference locstr dir s)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 6ec5ab9b4..7359b2e2a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -813,7 +813,7 @@ let instance sigma s c =
 let hnf_prod_app env sigma t n =
   match kind_of_term (whd_betadeltaiota env sigma 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_appvect env sigma t nl =
   Array.fold_left (hnf_prod_app env sigma) t nl
@@ -824,7 +824,7 @@ let hnf_prod_applist env sigma t nl =
 let hnf_lam_app env sigma t n =
   match kind_of_term (whd_betadeltaiota env sigma t) with
     | Lambda (_,_,b) -> subst1 n b
-    | _ -> anomaly "hnf_lam_app: Need an abstraction"
+    | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction")
 
 let hnf_lam_appvect env sigma t nl =
   Array.fold_left (hnf_lam_app env sigma) t nl
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index beb0be32f..b01e30bac 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
 open Errors
 open Util
 open Term
@@ -22,7 +23,7 @@ let rec subst_type env sigma typ = function
   | h::rest ->
       match kind_of_term (whd_betadeltaiota env sigma typ) with
         | Prod (na,c1,c2) -> subst_type env sigma (subst1 h c2) rest
-        | _ -> anomaly "Non-functional construction"
+        | _ -> anomaly (str "Non-functional construction")
 
 (* Si ft est le type d'un terme f, lequel est appliqué à args, *)
 (* [sort_of_atomic_ty] calcule ft[args] qui doit être une sorte *)
@@ -40,7 +41,7 @@ let sort_of_atomic_type env sigma ft args =
 let type_of_var env id =
   try let (_,_,ty) = lookup_named id env in ty
   with Not_found ->
-    anomaly ("type_of: variable "^(Id.to_string id)^" unbound")
+    anomaly ~label:"type_of" (str "variable " ++ Id.print id ++ str " unbound")
 
 let is_impredicative_set env = match Environ.engagement env with
 | Some ImpredicativeSet -> true
@@ -51,7 +52,7 @@ let retype ?(polyprop=true) sigma =
     match kind_of_term cstr with
     | Meta n ->
       (try strip_outer_cast (Evd.meta_ftype sigma n).Evd.rebus
-       with Not_found -> anomaly ("type_of: unknown meta " ^ string_of_int n))
+       with Not_found -> anomaly ~label:"type_of" (str "unknown meta " ++ int n))
     | Rel n ->
         let (_,_,ty) = lookup_rel n env in
         lift n ty
@@ -63,7 +64,7 @@ let retype ?(polyprop=true) sigma =
     | Case (_,p,c,lf) ->
         let Inductiveops.IndType(_,realargs) =
           try Inductiveops.find_rectype env sigma (type_of env c)
-          with Not_found -> anomaly "type_of: Bad recursive type" in
+          with Not_found -> anomaly ~label:"type_of" (str "Bad recursive type") in
         let t = whd_beta sigma (applist (p, realargs)) in
         (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with
           | Prod _ -> whd_beta sigma (applist (t, [c]))
@@ -104,7 +105,7 @@ let retype ?(polyprop=true) sigma =
         sort_of_atomic_type env sigma t args
     | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
     | Lambda _ | Fix _ | Construct _ ->
-        anomaly "sort_of: Not a type (1)"
+        anomaly ~label:"sort_of" (str "Not a type (1)")
     | _ -> decomp_sort env sigma (type_of env t)
 
   and sort_family_of env t =
@@ -122,7 +123,7 @@ let retype ?(polyprop=true) sigma =
     | App(f,args) ->
 	family_of_sort (sort_of_atomic_type env sigma (type_of env f) args)
     | Lambda _ | Fix _ | Construct _ ->
-        anomaly "sort_of: Not a type (1)"
+        anomaly ~label:"sort_of" (str "Not a type (1)")
     | _ -> family_of_sort (decomp_sort env sigma (type_of env t))
 
   and type_of_global_reference_knowing_parameters env c args =
@@ -132,11 +133,11 @@ let retype ?(polyprop=true) sigma =
       let (_,mip) = lookup_mind_specif env ind in
 	(try Inductive.type_of_inductive_knowing_parameters
 	       ~polyprop env mip argtyps
-	 with Reduction.NotArity -> anomaly "type_of: Not an arity")
+	 with Reduction.NotArity -> anomaly ~label:"type_of" (str "Not an arity"))
     | Const cst ->
       let t = constant_type env cst in
 	(try Typeops.type_of_constant_knowing_parameters env t argtyps
-	 with Reduction.NotArity -> anomaly "type_of: Not an arity")
+	 with Reduction.NotArity -> anomaly ~label:"type_of" (str "Not an arity"))
     | Var id -> type_of_var env id
     | Construct cstr -> type_of_constructor env cstr
     | _ -> assert false
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b265d636e..47c382c2e 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -99,7 +99,7 @@ let destEvalRef c = match kind_of_term c with
   | Var id  -> EvalVar id
   | Rel n -> EvalRel n
   | Evar ev -> EvalEvar ev
-  | _ -> anomaly "Not an unfoldable reference"
+  | _ -> anomaly (Pp.str "Not an unfoldable reference")
 
 let reference_opt_value sigma env = function
   | EvalConst cst -> constant_opt_value env cst
@@ -288,7 +288,7 @@ let compute_consteval_mutual_fix sigma env ref =
 	  (* Forget all \'s and args and do as if we had started with c' *)
 	  let ref = destEvalRef c' in
 	  (match reference_opt_value sigma env ref with
-	    | None -> anomaly "Should have been trapped by compute_direct"
+	    | None -> anomaly (Pp.str "Should have been trapped by compute_direct")
 	    | Some c -> srec env (minarg-nargs) [] ref c)
       | _ -> (* Should not occur *) NotAnElimination
   in
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 70843c7a9..d10289820 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -211,7 +211,7 @@ let push_named_rec_types (lna,typarray,_) env =
       (fun i na t ->
 	 match na with
 	   | Name id -> (id, None, lift i t)
-	   | Anonymous -> anomaly "Fix declarations must be named")
+	   | Anonymous -> anomaly (Pp.str "Fix declarations must be named"))
       lna typarray in
   Array.fold_left
     (fun e assum -> push_named assum e) env ctxt
@@ -275,7 +275,7 @@ let rec drop_extra_implicit_args c = match kind_of_term c with
 (* Get the last arg of an application *)
 let last_arg c = match kind_of_term c with
   | App (f,cl) -> Array.last cl
-  | _ -> anomaly "last_arg"
+  | _ -> anomaly (Pp.str "last_arg")
 
 (* Get the last arg of an application *)
 let decompose_app_vect c =
@@ -974,7 +974,7 @@ let rec eta_reduce_head c =
 	(match kind_of_term (eta_reduce_head c') with
            | App (f,cl) ->
                let lastn = (Array.length cl) - 1 in
-               if lastn < 1 then anomaly "application without arguments"
+               if lastn < 1 then anomaly (Pp.str "application without arguments")
                else
                  (match kind_of_term cl.(lastn) with
                     | Rel 1 ->
@@ -1043,7 +1043,7 @@ let adjust_subst_to_rel_context sign l =
     | (_,Some c,_)::sign', args' ->
 	aux (substl (List.rev subst) c :: subst) sign' args'
     | [], [] -> List.rev subst
-    | _ -> anomaly "Instance and signature do not match"
+    | _ -> anomaly (Pp.str "Instance and signature do not match")
   in aux [] (List.rev sign) l
 
 let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
@@ -1093,7 +1093,7 @@ let context_chop k ctx =
     | (0, l2) -> (List.rev acc, l2)
     | (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t)
     | (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
-    | (_, []) -> anomaly "context_chop"
+    | (_, []) -> anomaly (Pp.str "context_chop")
   in chop_aux [] (k,ctx)
 
 (* Do not skip let-in's *)
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index bff9bb499..0f9100e79 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
 open Errors
 open Util
 open Term
@@ -21,7 +22,7 @@ open Arguments_renaming
 let meta_type evd mv =
   let ty =
     try Evd.meta_ftype evd mv
-    with Not_found -> anomaly ("unknown meta ?"^Nameops.string_of_meta mv) in
+    with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv)) in
   meta_instance evd ty
 
 let constant_type_knowing_parameters env cst jl =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 87025b4d2..3a67a13ab 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -633,7 +633,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
       (list_of_app_stack ts) (list_of_app_stack ts1) with
       |Some substn ->
 	unirec_rec curenvnb pb b false substn c1 (applist (c,(List.rev ks)))
-      |None -> anomaly "As expected, solve_canonical_projection breaks the term too much"
+      |None -> anomaly (Pp.str "As expected, solve_canonical_projection breaks the term too much")
   in
   let evd = sigma in
     if (if occur_meta_or_undefined_evar evd m || occur_meta_or_undefined_evar evd n