Uniformization of the "anomaly" command.

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

26 files changed, 112 insertions, 110 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 21077ecc8..a85c80a79 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -51,7 +51,7 @@ module ST=struct
 
   let enter t sign st=
     if Hashtbl.mem st.toterm sign then
-	anomaly "enter: signature already entered"
+	anomaly ~label:"enter" (Pp.str "signature already entered")
     else
 	Hashtbl.replace st.toterm sign t;
 	Hashtbl.replace st.tosign t sign
@@ -272,7 +272,7 @@ let find uf i= find_aux uf [] i
 let get_representative uf i=
   match uf.map.(i).clas with
       Rep r -> r
-    | _ -> anomaly "get_representative: not a representative"
+    | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative")
 
 let find_pac uf i pac =
   PacMap.find pac (get_representative uf i).constructors
@@ -280,7 +280,7 @@ let find_pac uf i pac =
 let get_constructor_info uf i=
   match uf.map.(i).term with
       Constructor cinfo->cinfo
-    | _ -> anomaly "get_constructor: not a constructor"
+    | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor")
 
 let size uf i=
   (get_representative uf i).weight
@@ -325,7 +325,7 @@ let term uf i=uf.map.(i).term
 let subterms uf i=
   match uf.map.(i).vertex with
       Node(j,k) -> (j,k)
-    | _ -> anomaly "subterms: not a node"
+    | _ -> anomaly ~label:"subterms" (Pp.str "not a node")
 
 let signature uf i=
   let j,k=subterms uf i in (find uf j,find uf k)
@@ -402,7 +402,7 @@ let rec canonize_name c =
 let build_subst uf subst =
   Array.map (fun i ->
 	       try term uf i
-	       with _ -> anomaly "incomplete matching") subst
+	       with _ -> anomaly (Pp.str "incomplete matching")) subst
 
 let rec inst_pattern subst = function
     PVar i ->
@@ -657,8 +657,8 @@ let process_constructor_mark t i rep pac state =
 			{lhs=s1;rhs=s2;rule=Injection(s,opac,t,pac,n)}
 			state.combine;
 		      f (n-1) q1 q2
-		  | _-> anomaly
-		      "add_pacs : weird error in injection subterms merge"
+		  | _-> anomaly ~label:"add_pacs"
+		      (Pp.str "weird error in injection subterms merge")
 	    in f cinfo.ci_nhyps opac.args pac.args
       | Partial_applied | Partial _ ->
 	  add_pac rep pac t;
@@ -750,7 +750,7 @@ let complete_one_class state i=
 	let ct = app (term state.uf i) typ pac.arity in
 	  state.uf.epsilons <- pac :: state.uf.epsilons;
 	  ignore (add_term state ct)
-    | _ -> anomaly "wrong incomplete class"
+    | _ -> anomaly (Pp.str "wrong incomplete class")
 
 let complete state =
   Int.Set.iter (complete_one_class state) state.pa_classes
@@ -890,7 +890,7 @@ let find_instances state =
 	check_for_interrupt ();
 	do_match state res pb_stack
       done;
-      anomaly "get out of here !"
+      anomaly (Pp.str "get out of here !")
     with Stack.Empty -> () in
     !res
 
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 25c01f2bd..5244dcf17 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -47,7 +47,7 @@ let rec ptrans p1 p3=
 	{p_lhs=p1.p_lhs;
 	 p_rhs=p3.p_rhs;
 	 p_rule=Trans (p1,p3)}
-      else anomaly "invalid cc transitivity"
+      else anomaly (Pp.str "invalid cc transitivity")
 
 let rec psym p =
   match p.p_rule with
@@ -85,7 +85,7 @@ let rec nth_arg t n=
 	if n>0 then
 	  nth_arg t1 (n-1)
 	else t2
-    | _ -> anomaly "nth_arg: not enough args"
+    | _ -> anomaly ~label:"nth_arg" (Pp.str "not enough args")
 
 let pinject p c n a =
   {p_lhs=nth_arg p.p_lhs (n-a);
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index eb7d9e8e4..3cc0686ad 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -237,7 +237,7 @@ let rec deanonymize ids =
 
 let rec glob_of_pat =
   function
-      PatVar (loc,Anonymous) -> anomaly "Anonymous pattern variable"
+      PatVar (loc,Anonymous) -> anomaly (Pp.str "Anonymous pattern variable")
     | PatVar (loc,Name id) ->
 	  GVar (loc,id)
     | PatCstr(loc,((ind,_) as cstr),lpat,_) ->
@@ -288,10 +288,10 @@ let bind_aliases patvars subst patt =
 let interp_pattern env pat_expr =
   let patvars,pats = Constrintern.intern_pattern env pat_expr in
     match pats with
-	[] -> anomaly "empty pattern list"
+	[] -> anomaly (Pp.str "empty pattern list")
       | [subst,patt] ->
 	  (patvars,bind_aliases patvars subst patt,patt)
-      | _  -> anomaly "undetected disjunctive pattern"
+      | _  -> anomaly (Pp.str "undetected disjunctive pattern")
 
 let rec match_args dest names constr = function
     [] -> [],names,substl names constr
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index a42e0cb3e..c25a150f4 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -177,7 +177,7 @@ let close_block bt pts =
 		ET_Case_analysis -> error "\"end cases\" expected."
 	      | ET_Induction ->  error "\"end induction\" expected."
 	  end
-      | _,_ -> anomaly "Lonely suppose on stack."
+      | _,_ -> anomaly (Pp.str "Lonely suppose on stack.")
 
 
 (* utility for suppose / suppose it is *)
@@ -187,7 +187,7 @@ let close_previous_case pts =
     Proof.is_done pts
   then
     match get_top_stack pts with
-	Per (et,_,_,_) :: _ -> anomaly "Weird case occured ..."
+	Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occured ...")
       | Suppose_case :: Per (et,_,_,_) :: _ ->
 	  goto_current_focus (pts)
       | _ -> error "Not inside a proof per cases or induction."
@@ -233,7 +233,7 @@ let prepare_goal items gls =
        filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls
 
 let my_automation_tac = ref
-  (fun gls -> anomaly "No automation registered")
+  (fun gls -> anomaly (Pp.str "No automation registered"))
 
 let register_automation_tac tac = my_automation_tac:= tac
 
@@ -380,7 +380,7 @@ let concl_refiner metas body gls =
   let env = pf_env gls in
   let sort = family_of_sort (Typing.sort_of env evd concl) in
   let rec aux env avoid subst = function
-      [] -> anomaly "concl_refiner: cannot happen"
+      [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen")
     | (n,typ)::rest ->
 	let _A = subst_meta subst typ in
 	let x = id_of_name_using_hdchar env _A Anonymous in
@@ -896,7 +896,7 @@ let register_nodep_subcase id= function
 	  | EK_nodep -> clauses,Per(et,pi,EK_nodep,id::clauses)::s
 	  | EK_dep _ -> error "Do not mix \"suppose\" with \"suppose it is\"."
       end
-  | _ -> anomaly "wrong stack state"
+  | _ -> anomaly (Pp.str "wrong stack state")
 
 let suppose_tac hyps gls0 =
   let info = get_its_info gls0 in
@@ -950,7 +950,7 @@ let rec add_branch ((id,_) as cpl) pats tree=
 	  match tree with
 	      End_patt cpl0 -> End_patt cpl0
 		(* this ensures precedence for overlapping patterns *)
-	    | _ -> anomaly "tree is expected to end here"
+	    | _ -> anomaly (Pp.str "tree is expected to end here")
 	end
     | args::stack ->
 	match args with
@@ -959,7 +959,7 @@ let rec add_branch ((id,_) as cpl) pats tree=
 		match tree with
 		   Close_patt t ->
 		     Close_patt (add_branch cpl stack t)
-		  | _ -> anomaly "we should pop here"
+		  | _ -> anomaly (Pp.str "we should pop here")
 	      end
 	  | (patt,rp) :: rest_args ->
 	      match patt with
@@ -974,7 +974,7 @@ let rec add_branch ((id,_) as cpl) pats tree=
 			      (fun i bri ->
 				 append_branch cpl 1 (rest_args::stack) bri)
 			      tree
-			| _ -> anomaly "No pop/stop expected here"
+			| _ -> anomaly (Pp.str "No pop/stop expected here")
 		    end
 		| PatCstr (_,(ind,cnum),args,nam) ->
 		      match tree with
@@ -1002,7 +1002,7 @@ let rec add_branch ((id,_) as cpl) pats tree=
 				  (nargs::rest_args::stack) bri
 			    else bri in
 			    map_tree_rp rp (fun ids -> ids) mapi tree
-		      | _ -> anomaly "No pop/stop expected here"
+		      | _ -> anomaly (Pp.str "No pop/stop expected here")
 and append_branch ((id,_) as cpl) depth pats = function
     Some (ids,tree) ->
       Some (Id.Set.add id ids,append_tree cpl depth pats tree)
@@ -1015,7 +1015,7 @@ and append_tree ((id,_) as cpl) depth pats tree =
 	Close_patt (append_tree cpl (pred depth) pats t)
     | Skip_patt (ids,t) ->
 	Skip_patt (Id.Set.add id ids,append_tree cpl depth pats t)
-    | End_patt _ -> anomaly "Premature end of branch"
+    | End_patt _ -> anomaly (Pp.str "Premature end of branch")
     | Split_patt (_,_,_) ->
 	map_tree (Id.Set.add id)
 	  (fun i bri -> append_branch cpl (succ depth) pats bri) tree
@@ -1105,7 +1105,7 @@ let case_tac params pat_info hyps gls0 =
   let et,per_info,ek,old_clauses,rest =
     match info.pm_stack with
 	Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest)
-      | _ -> anomaly "wrong place for cases" in
+      | _ -> anomaly (Pp.str "wrong place for cases") in
   let clause = build_dep_clause params pat_info per_info hyps gls0 in
   let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
   let nek = 
@@ -1130,7 +1130,7 @@ let initial_instance_stack ids : (_, _) instance_stack =
   List.map (fun id -> id,[None,[]]) ids
 
 let push_one_arg arg = function
-    [] -> anomaly "impossible"
+    [] -> anomaly (Pp.str "impossible")
   | (head,args) :: ctx ->
       ((head,(arg::args)) :: ctx)
 
@@ -1148,7 +1148,7 @@ let push_head c ids stacks =
 let pop_one (id,stack) =
   let nstack=
     match stack with
-	[] -> anomaly "impossible"
+	[] -> anomaly (Pp.str "impossible")
       | [c] as l -> l
       | (Some head,args)::(head0,args0)::ctx ->
 	  let arg = applist (head,(List.rev args)) in
@@ -1195,7 +1195,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 		       (applist (mkVar id,
 				 List.append param_metas 
 				   (List.rev_append br_args hyp_metas)))) gls
-	    | _ -> anomaly "wrong stack size"
+	    | _ -> anomaly (Pp.str "wrong stack size")
 	end
     | Split_patt (ids,ind,br), casee::next_objs ->
 	let (mind,oind) as spec = Global.lookup_inductive ind in
@@ -1262,11 +1262,11 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	    (refine case_term)
 	    (Array.mapi branch_tac br) gls
     | Split_patt (_, _, _) , [] ->
-	anomaly "execute_cases : Nothing to split"
+	anomaly ~label:"execute_cases " (Pp.str "Nothing to split")
     | Skip_patt _ , [] ->
-	anomaly "execute_cases : Nothing to skip"
+	anomaly ~label:"execute_cases " (Pp.str "Nothing to skip")
     | End_patt (_,_) , _ :: _  ->
-	anomaly "execute_cases : End of branch with garbage left"
+	anomaly ~label:"execute_cases " (Pp.str "End of branch with garbage left")
 
 let understand_my_constr c gls =
   let env = pf_env gls in
@@ -1289,14 +1289,14 @@ let end_tac et2 gls =
   let et1,pi,ek,clauses =
     match info.pm_stack with
 	Suppose_case::_ ->
-	  anomaly "This case should already be trapped"
+	  anomaly (Pp.str "This case should already be trapped")
       | Claim::_ ->
 	  error "\"end claim\" expected."
       | Focus_claim::_ ->
 	  error "\"end focus\" expected."
       | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses)
       | [] ->
-	  anomaly "This case should already be trapped" in
+	  anomaly (Pp.str "This case should already be trapped") in
   let et =
     if et1 <> et2 then
       match et1 with
@@ -1394,7 +1394,7 @@ let rec do_proof_instr_gen _thus _then instr =
     | Psuppose hyps      -> suppose_tac hyps
     | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps
     | Pend (B_elim et) -> end_tac et
-    | Pend _ -> anomaly "Not applicable"
+    | Pend _ -> anomaly (Pp.str "Not applicable")
     | Pescape -> escape_tac
 
 let eval_instr {instr=instr} =
@@ -1443,7 +1443,7 @@ let rec postprocess pts instr =
  	    with
 		Type_errors.TypeError(env,
 				      Type_errors.IllFormedRecBody(_,_,_,_,_)) ->
-		  anomaly "\"end induction\" generated an ill-formed fixpoint"
+		  anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint")
 	end
     | Pend _ ->
 	goto_current_focus_or_top (pts)
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index c2b286f1b..0b7e94fa0 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -44,15 +44,15 @@ let pr_open_subgoals () =
 *)
 
 let pr_proof_instr instr = 
-  Errors.anomaly "Cannot print a proof_instr"
+  Errors.anomaly (Pp.str "Cannot print a proof_instr")
     (* arnaud: Il nous faut quelque chose de type extr_genarg_printer si on veut aller
                      dans cette direction
        Ppdecl_proof.pr_proof_instr (Global.env()) instr
     *)
 let pr_raw_proof_instr instr =
-  Errors.anomaly "Cannot print a raw proof_instr"
+  Errors.anomaly (Pp.str "Cannot print a raw proof_instr")
 let pr_glob_proof_instr instr =
-  Errors.anomaly "Cannot print a non-interpreted proof_instr"
+  Errors.anomaly (Pp.str "Cannot print a non-interpreted proof_instr")
 
 let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }=
   Decl_interp.interp_proof_instr 
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index 01f32e4a3..7f63c4200 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -75,7 +75,7 @@ and print_vars pconstr gtyp env sep _be _have vars =
       begin
 	let nenv =
 	  match st.st_label with
-	      Anonymous -> anomaly "anonymous variable"
+	      Anonymous -> anomaly (Pp.str "anonymous variable")
 	    | Name id -> Environ.push_named (id,None,st.st_it) env in
 	let pr_sep = if sep then pr_comma () else mt () in
 		spc() ++ pr_sep ++
@@ -173,14 +173,14 @@ let rec pr_bare_proof_instr _then _thus env = function
       str "per" ++ spc () ++ pr_elim_type et ++ spc () ++
       pr_casee env c
   | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et
-  | _ -> anomaly "unprintable instruction"
+  | _ -> anomaly (Pp.str "unprintable instruction")
 
 let pr_emph = function
     0 -> str "    "
   | 1 -> str "*   "
   | 2 -> str "**  "
   | 3 -> str "*** "
-  | _ -> anomaly "unknown emphasis"
+  | _ -> anomaly (Pp.str "unknown emphasis")
 
 let pr_proof_instr env instr =
   pr_emph instr.emph ++ spc () ++
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 7f5ad4f66..85b9bde71 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -348,7 +348,7 @@ and extract_seb env mp all = function
   | SEBstruct (msb) ->
       let env' = Modops.add_signature mp msb empty_delta_resolver env in
       MEstruct (mp,extract_sfb env' mp all msb)
-  | SEBwith (_,_) -> anomaly "Not available yet"
+  | SEBwith (_,_) -> anomaly (Pp.str "Not available yet")
 
 and extract_module env mp all mb =
   (* A module has an empty [mod_expr] when :
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 43a08657b..eb166675e 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -19,7 +19,7 @@ open Mlutil
 let rec msid_of_mt = function
   | MTident mp -> mp
   | MTwith(mt,_)-> msid_of_mt mt
-  | _ -> anomaly "Extraction:the With operator isn't applied to a name"
+  | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name")
 
 (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a
    [ml_structure]. *)
@@ -226,7 +226,7 @@ let get_decl_in_structure r struc =
 		  | _ -> error_not_visible r
     in go ll sel
   with Not_found ->
-    anomaly "reference not found in extracted structure"
+    anomaly (Pp.str "reference not found in extracted structure")
 
 
 (*s Optimization of a [ml_structure]. *)
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 74728f412..51946871f 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -242,7 +242,7 @@ let safe_basename_of_global r =
   let last_chance r =
     try Nametab.basename_of_global r
     with Not_found ->
-      anomaly "Inductive object unknown to extraction and not globally visible"
+      anomaly (Pp.str "Inductive object unknown to extraction and not globally visible")
   in
   match r with
     | ConstRef kn -> Label.to_id (con_label kn)
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index c7a582a0e..d39c6167b 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -75,7 +75,7 @@ let match_one_quantified_hyp setref seq lf=
       Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))->
 	if do_sequent setref triv lf.id seq i dom lf.atoms then
 	  setref:=IS.add ((Phantom dom),lf.id) !setref
-    | _ ->anomaly "can't happen"
+    | _ -> anomaly (Pp.str "can't happen")
 
 let give_instances lf seq=
   let setref=ref IS.empty in
@@ -125,7 +125,7 @@ let mk_open_instance id gl m t=
 	  GLambda(loc,name,k,_,t0)->
 	    let t1=raux (n-1) t0 in
 	      GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name),t1)
-	| _-> anomaly "can't happen" in
+	| _-> anomaly (Pp.str "can't happen") in
   let ntt=try
     Pretyping.understand evmap env (raux m rawt)
   with _ ->
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 7acabaaa4..c812deaf5 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -32,7 +32,7 @@ let wrap n b continue seq gls=
   let rec aux i nc ctx=
     if i<=0 then seq else
       match nc with
-	  []->anomaly "Not the expected number of hyps"
+	  []->anomaly (Pp.str "Not the expected number of hyps")
 	| ((id,_,typ) as nd)::q->
 	    if occur_var env id (pf_concl gls) ||
 	      List.exists (occur_var_in_decl env id) ctx then
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 9c895e6a9..450b3ef40 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -310,7 +310,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
 	(fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) ->
 	   try
 	     let witness = Int.Map.find i sub in
-	     if b' <> None then anomaly "can not redefine a rel!";
+	     if b' <> None then anomaly (Pp.str "can not redefine a rel!");
 	     (Termops.pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun))
 	   with Not_found  ->
 	     (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
@@ -396,7 +396,7 @@ let rewrite_until_var arg_num eq_ids : tactic =
     then tclIDTAC g
     else
       match eq_ids with
-	| [] -> anomaly "Cannot find a way to prove recursive property";
+	| [] -> anomaly (Pp.str "Cannot find a way to prove recursive property");
 	| eq_id::eq_ids ->
 	    tclTHEN
 	      (tclTRY (Equality.rewriteRL (mkVar eq_id)))
@@ -604,7 +604,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 		   observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++
 			      pr_lconstr_env (pf_env g') new_term_value_eq
 			   );
-		   anomaly "cannot compute new term value"
+		   anomaly (Pp.str "cannot compute new term value")
 	   in
 	 let fun_body =
 	   mkLambda(Anonymous,
@@ -830,7 +830,7 @@ let build_proof
 		 h_reduce_with_zeta Locusops.onConcl;
 		 build_proof do_finalize new_infos
 		] g
-	  | Rel _ -> anomaly "Free var in goal conclusion !"
+	  | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !")
   and build_proof do_finalize dyn_infos g =
 (*     observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
     observe_tac_stream (str "build_proof with " ++ Printer.pr_lconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
@@ -1014,7 +1014,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
 		{finfos with
 		   equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
 					      ConstRef c -> c
-					    | _ -> Errors.anomaly "Not a constant"
+					    | _ -> Errors.anomaly (Pp.str "Not a constant")
 					 )
 		}
 	  | _ -> ()
@@ -1208,7 +1208,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	    else
 	      h_mutual_fix this_fix_info.name (this_fix_info.idx + 1)
 		other_fix_infos
-	| _ -> anomaly "Not a valid information"
+	| _ -> anomaly (Pp.str "Not a valid information")
     in
     let first_tac : tactic = (* every operations until fix creations *)
       tclTHENSEQ
@@ -1223,7 +1223,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	let ctxt,pte_app =  (decompose_prod_assum (pf_concl gl)) in
 	let pte,pte_args = (decompose_app pte_app) in
 	try
-	  let pte = try destVar pte with _ -> anomaly "Property is not a variable"  in
+	  let pte = try destVar pte with _ -> anomaly (Pp.str "Property is not a variable")  in
 	  let fix_info = Id.Map.find  pte ptes_to_fix in
 	  let nb_args = fix_info.nb_realargs in
 	  tclTHENSEQ
@@ -1364,7 +1364,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 
 let prove_with_tcc tcc_lemma_constr eqs : tactic =
   match !tcc_lemma_constr with
-    | None -> anomaly "No tcc proof !!"
+    | None -> anomaly (Pp.str "No tcc proof !!")
     | Some lemma ->
 	fun gls ->
 (* 	  let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *)
@@ -1562,7 +1562,7 @@ let prove_principle_for_gen
   let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in
   let lemma =
     match !tcc_lemma_ref with
-     | None -> anomaly ( "No tcc proof !!")
+     | None -> anomaly (str "No tcc proof !!")
      | Some lemma -> lemma
   in
 (*   let rec list_diff del_list check_list = *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 700beaff5..9916ed95a 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -48,7 +48,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
        let id =  Namegen.next_ident_away x avoid in
        Hashtbl.add tbl id x;
        (Name id,v,t)::(change_predicates_names (id::avoid) predicates)
-    | (Anonymous,_,_)::_ -> anomaly "Anonymous property binder "
+    | (Anonymous,_,_)::_ -> anomaly (Pp.str "Anonymous property binder ")
   in
   let avoid = (Termops.ids_of_context env_with_params ) in
   let princ_type_info =
@@ -395,7 +395,7 @@ let get_funs_constant mp dp =
 		     let const = make_con mp dp (Label.of_id id) in
 		     const,i
 		 | Anonymous ->
-		     anomaly "Anonymous fix"
+		     anomaly (Pp.str "Anonymous fix")
 	    )
 	    na
       | _ -> [|const,0|]
@@ -505,7 +505,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
   let first_type,other_princ_types =
     match l_schemes with
 	s::l_schemes -> s,l_schemes
-      | _ -> anomaly ""
+      | _ -> anomaly (Pp.str "")
   in
   let (_,(const,_,_)) =
     try
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 8acd24c88..9ec935cfd 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1092,7 +1092,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
 		else
 		  GProd(Loc.ghost,n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
-	    | _ -> anomaly "Should not have an anonymous function here"
+	    | _ -> anomaly (Pp.str "Should not have an anonymous function here")
 		(* We have renamed all the anonymous functions during alpha_renaming phase *)
 
 	end
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index a74ae84e2..868bf58c9 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -532,7 +532,7 @@ let rec are_unifiable_aux  = function
 	     else
 	       let eqs' =
  		 try  ((List.combine cpl1 cpl2)@eqs)
-		 with _ -> anomaly "are_unifiable_aux"
+		 with _ -> anomaly (Pp.str "are_unifiable_aux")
 	       in
 	       are_unifiable_aux eqs'
 
@@ -554,7 +554,7 @@ let rec eq_cases_pattern_aux  = function
 	     else
 	       let eqs' =
  		 try  ((List.combine cpl1 cpl2)@eqs)
-		 with _ -> anomaly "eq_cases_pattern_aux"
+		 with _ -> anomaly (Pp.str "eq_cases_pattern_aux")
 	       in
 	       eq_cases_pattern_aux eqs'
 	 | _ -> raise NotUnifiable
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 6c3b009f8..850234c3b 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -641,7 +641,7 @@ let rec add_args id new_args b =
 	    CAppExpl(Loc.ghost,(None,r),new_args)
 	| _ -> b
       end
-  | CFix  _  | CCoFix _ -> anomaly "add_args : todo"
+  | CFix  _  | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo")
   | CProdN(loc,nal,b1) ->
       CProdN(loc,
 	     List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
@@ -692,10 +692,10 @@ let rec add_args id new_args b =
       CRecord (loc,
 	       (match w with Some w -> Some (add_args id new_args w) | _ -> None),
 	       List.map (fun (e,o) -> e, add_args id new_args o) pars)
-  | CNotation _ -> anomaly "add_args : CNotation"
-  | CGeneralization _ -> anomaly "add_args : CGeneralization"
+  | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation")
+  | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization")
   | CPrim _ -> b
-  | CDelimiters _ -> anomaly "add_args : CDelimiters"
+  | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters")
 exception Stop of  Constrexpr.constr_expr
 
 
@@ -736,7 +736,7 @@ let rec chop_n_arrow n t =
 	      chop_n_arrow new_n t'
 	    with Stop t -> t
 	  end
-      | _ -> anomaly "Not enough products"
+      | _ -> anomaly (Pp.str "Not enough products")
 
 
 let rec get_args b t : Constrexpr.local_binder list *
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index dfbfdce3a..a041205bf 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -389,7 +389,7 @@ let _ =
 
 let find_or_none id =
   try Some
-    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly "Not a constant"
+    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly (Pp.str "Not a constant")
     )
   with Not_found -> None
 
@@ -417,7 +417,7 @@ let add_Function is_general f =
   and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
   and graph_ind =
     match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
-    with | IndRef ind -> ind | _ -> Errors.anomaly "Not an inductive"
+    with | IndRef ind -> ind | _ -> Errors.anomaly (Pp.str "Not an inductive")
   in
   let finfos =
     { function_constant = f;
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index eed421159..a061cfaca 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -112,7 +112,7 @@ let generate_type g_to_f f graph i =
   let ctxt,_ = decompose_prod_assum graph_arity in
   let fun_ctxt,res_type =
     match ctxt with
-      | [] | [_] -> anomaly "Not a valid context"
+      | [] | [_] -> anomaly (Pp.str "Not a valid context")
       | (_,_,res_type)::fun_ctxt -> fun_ctxt,res_type
   in
   let rec args_from_decl i accu = function
@@ -277,7 +277,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	(fun (_,pat) acc ->
 	     match pat with
 	       | Genarg.IntroIdentifier id -> Id.Set.add id acc
-	| _ -> anomaly "Not an identifier"
+	| _ -> anomaly (Pp.str "Not an identifier")
 	)
 	(List.nth intro_pats (pred i))
 	Id.Set.empty
@@ -316,7 +316,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       	  (fun (_,pat) acc ->
       	     match pat with
 	       | IntroIdentifier id -> id::acc
-      	       | _ -> anomaly "Not an identifier"
+      	       | _ -> anomaly (Pp.str "Not an identifier")
       	  )
       	  (List.nth intro_pats (pred i))
       	  []
@@ -423,7 +423,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       Array.map
 	(fun (_,(ctxt,concl)) ->
 	   match ctxt with
-	     | [] | [_] | [_;_] -> anomaly "bad context"
+	     | [] | [_] | [_;_] -> anomaly (Pp.str "bad context")
 	     | hres::res::(x,_,t)::ctxt ->
 		 Termops.it_mkLambda_or_LetIn
 		   (Termops.it_mkProd_or_LetIn concl [hres;res])
@@ -488,7 +488,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       Array.map
 	(fun (_,(ctxt,concl)) ->
 	   match ctxt with
-	     | [] | [_] | [_;_] -> anomaly "bad context"
+	     | [] | [_] | [_;_] -> anomaly (Pp.str "bad context")
 	     | hres::res::(x,_,t)::ctxt ->
 		 Termops.it_mkLambda_or_LetIn
 		   (Termops.it_mkProd_or_LetIn concl [hres;res])
@@ -541,7 +541,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	  (fun (_,pat) acc ->
 	     match pat with
 	       | Genarg.IntroIdentifier id -> Id.Set.add id acc
-	       | _ -> anomaly "Not an identifier"
+	       | _ -> anomaly (Pp.str "Not an identifier")
 	  )
 	  (List.nth intro_pats (pred i))
 	  Id.Set.empty
@@ -935,7 +935,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
       then
 	let eq_lemma =
 	  try Option.get (infos).equation_lemma
-	  with Option.IsNone -> anomaly "Cannot find equation lemma"
+	  with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma")
 	in
 	tclTHENSEQ[
 	  tclMAP h_intro ids;
@@ -1146,7 +1146,7 @@ let revert_graph kn post_tac hid g =
 	    let info =
 	      try find_Function_of_graph ind'
 	      with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*)
-		anomaly "Cannot retrieve infos about a mutual block"
+		anomaly (Pp.str "Cannot retrieve infos about a mutual block")
 	    in
 	    (* if we can find a completeness lemma for this function
 	       then we can come back to the functional form. If not, we do nothing
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 4b87a9b9c..8816d960f 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -73,8 +73,8 @@ let def_of_const t =
              | Some c -> Declarations.force c
 	     | _ -> assert false)
        with _ ->
-	 anomaly ("Cannot find definition of constant "^
-		    (Id.to_string (Label.to_id (con_label sp))))
+	 anomaly (str "Cannot find definition of constant " ++
+		    (Id.print (Label.to_id (con_label sp))))
       )
      |_ -> assert false
 
@@ -91,7 +91,7 @@ let constant sl s =
 	       (Id.of_string s)));;
 let const_of_ref = function
     ConstRef kn -> kn
-  | _ -> anomaly "ConstRef expected"
+  | _ -> anomaly (Pp.str "ConstRef expected")
 
 
 let nf_zeta env =
@@ -426,7 +426,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	travel jinfo new_continuation_tac 
 	  {expr_info with info = b; is_final=false}
       end
-    | Rel _ -> anomaly "Free var in goal conclusion !"
+    | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !")
     | Prod _ -> 
       begin
 	try
@@ -1115,7 +1115,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
       let f_id =
 	match f_name with
 	  | Name f_id -> next_ident_away_in_goal f_id ids
-	  | Anonymous -> anomaly "Anonymous function"
+	  | Anonymous -> anomaly (Pp.str "Anonymous function")
       in
       let n_names_types,_ = decompose_lam_n nb_args body1 in
       let n_ids,ids =
@@ -1125,7 +1125,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
 	       | Name id ->
 		   let n_id = next_ident_away_in_goal id ids in
 		   n_id::n_ids,n_id::ids
-	       | _ -> anomaly "anonymous argument"
+	       | _ -> anomaly (Pp.str "anonymous argument")
 	  )
 	  ([],(f_id::ids))
 	  n_names_types
@@ -1249,7 +1249,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     | Some s -> s
     | None   ->
 	try (add_suffix current_proof_name "_subproof")
-	with _ -> anomaly "open_new_goal with an unamed theorem"
+	with _ -> anomaly (Pp.str "open_new_goal with an unamed theorem")
   in
   let sign = initialize_named_context_for_proof () in
   let na = next_global_ident_away name [] in
@@ -1261,7 +1261,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
       let na_global = Nametab.global na_ref in
       match na_global with
 	  ConstRef c -> is_opaque_constant c
-	| _ -> anomaly "equation_lemma: not a constant"
+	| _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant")
     in
     let lemma = mkConst (Lib.make_con na) in
     ref_ := Some lemma ;
@@ -1405,7 +1405,7 @@ let (com_eqn : int -> Id.t ->
     let opacity =
       match terminate_ref with
 	| ConstRef c -> is_opaque_constant c
-	| _ -> anomaly "terminate_lemma: not a constant"
+	| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant")
     in
     let (evmap, env) = Lemmas.get_current_context() in
     let f_constr = constr_of_global f_ref in
@@ -1499,7 +1499,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
 	begin
 	  if do_observe ()
 	  then msg_debug (str "Cannot create equation Lemma " ++ Errors.print e)
-	  else anomaly "Cannot create equation Lemma"
+	  else anomaly (Pp.str "Cannot create equation Lemma")
 	  ;
 	  true
 	end
@@ -1533,7 +1533,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   with e ->
     begin
       (try ignore (Backtrack.backto previous_label) with _ -> ());
-      (*       anomaly "Cannot create termination Lemma" *)
+      (*       anomaly (Pp.str "Cannot create termination Lemma") *)
       raise e
     end
 
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index eb713f251..a17c62eba 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -20,7 +20,7 @@ open Errors
 open Misctypes
 
 let out_arg = function
-  | ArgVar _ -> anomaly "Unevaluated or_var variable"
+  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
   | ArgArg x -> x
 
 TACTIC EXTEND PsatzZ
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 851516945..c4961654d 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -318,7 +318,7 @@ let coq_iff = lazy (constant "iff")
 let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with
   | Const kn when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) ->
       EvalConstRef kn
-  | _ -> anomaly ("Coq_omega: "^s^" is not an evaluable constant")
+  | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant"))
 
 let sp_Zsucc =     lazy (evaluable_ref_of_constr "Z.succ" coq_Zsucc)
 let sp_Zpred =     lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred)
@@ -578,7 +578,7 @@ let compile name kind =
 	let id = new_id () in
 	tag_hypothesis name id;
 	{kind = kind; body = List.rev accu; constant = n; id = id}
-    | _ -> anomaly "compile_equation"
+    | _ -> anomaly (Pp.str "compile_equation")
   in
   loop []
 
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 4238037e7..2c41b95f3 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -410,7 +410,7 @@ let quote_terms ivs lc gl =
                | None ->
                    begin match ivs.constant_lhs with
                      | Some c_lhs -> Termops.subst_meta [1, c] c_lhs
-                     | None -> anomaly "invalid inversion scheme for quote"
+                     | None -> anomaly (Pp.str "invalid inversion scheme for quote")
                    end
                | Some var_lhs ->
                    begin match ivs.constant_lhs with
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 5cb97d4bd..1b9afb7c7 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -122,7 +122,7 @@ let add_step s sub =
     | SI_Or_r,[p] -> I_Or_r p
     | SE_Or i,[p1;p2] -> E_Or(i,p1,p2)
     | SD_Or i,[p] -> D_Or(i,p)
-    | _,_ -> anomaly "add_step: wrong arity"
+    | _,_ -> anomaly ~label:"add_step" (Pp.str "wrong arity")
 
 type 'a with_deps =
     {dep_it:'a;
@@ -144,7 +144,7 @@ type state =
 
 let project = function
     Complete prf -> prf
-  | Incomplete (_,_) -> anomaly "not a successful state"
+  | Incomplete (_,_) -> anomaly (Pp.str "not a successful state")
 
 let pop n prf =
   let nprf=
@@ -338,7 +338,7 @@ let search_norev seq=
 		     (Arrow(f2,f3)))
 		  f1;
 		add_hyp (embed nseq) f3]):: !goals
-      | _ -> anomaly "search_no_rev: can't happen" in
+      | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen") in
     Int.Map.iter add_one seq.norev_hyps;
     List.rev !goals
 
@@ -363,7 +363,7 @@ let search_in_rev_hyps seq=
 	| Arrow (Disjunct (f1,f2),f0) ->
 	    [make_step (SD_Or(i)),
 	     [add_hyp (add_hyp (embed nseq) (Arrow(f1,f0))) (Arrow (f2,f0))]]
-	| _ -> anomaly "search_in_rev_hyps: can't happen"
+	| _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen")
   with
       Not_found -> search_norev seq
 
@@ -441,7 +441,7 @@ let branching = function
 	  | _::next ->
 	      s_info.nd_branching<-s_info.nd_branching+List.length next in
 	List.map (append stack) successors
-  | Complete prf -> anomaly "already succeeded"
+  | Complete prf -> anomaly (Pp.str "already succeeded")
 
 open Pp
 
diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4
index 34bb1d51f..9d3a10dba 100644
--- a/plugins/xml/acic2Xml.ml4
+++ b/plugins/xml/acic2Xml.ml4
@@ -21,7 +21,7 @@ let typesdtdname = "http://mowgli.cs.unibo.it/dtd/cictypes.dtd";;
 
 let rec find_last_id =
  function
-    [] -> Errors.anomaly "find_last_id: empty list"
+    [] -> Errors.anomaly ~label:"find_last_id" (Pp.str "empty list")
   | [id,_,_] -> id
   | _::tl -> find_last_id tl
 ;;
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 4a8436d76..2772779d4 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -12,6 +12,8 @@
 (*                       http://helm.cs.unibo.it                        *)
 (************************************************************************)
 
+open Pp
+
 (* Utility Functions *)
 
 exception TwoModulesWhoseDirPathIsOneAPrefixOfTheOther;;
@@ -162,7 +164,7 @@ let family_of_term ty =
  match Term.kind_of_term ty with
     Term.Sort s -> Coq_sort (Term.family_of_sort s)
   | Term.Const _ -> CProp  (* I could check that the constant is CProp *)
-  | _ -> Errors.anomaly "family_of_term"
+  | _ -> Errors.anomaly (Pp.str "family_of_term")
 ;;
 
 module CPropRetyping =
@@ -177,7 +179,7 @@ module CPropRetyping =
   | h::rest ->
       match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma typ) with
         | T.Prod (na,c1,c2) -> subst_type env sigma (T.subst1 h c2) rest
-        | _ -> Errors.anomaly "Non-functional construction"
+        | _ -> Errors.anomaly (Pp.str "Non-functional construction")
 
 
   let sort_of_atomic_type env sigma ft args =
@@ -193,7 +195,7 @@ let typeur sigma metamap =
     match Term.kind_of_term cstr with
     | T.Meta n ->
           (try T.strip_outer_cast (List.assoc n metamap)
-           with Not_found -> Errors.anomaly "type_of: this is not a well-typed term")
+           with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term"))
     | T.Rel n ->
         let (_,_,ty) = Environ.lookup_rel n env in
         T.lift n ty
@@ -202,7 +204,7 @@ let typeur sigma metamap =
           let (_,_,ty) = Environ.lookup_named id env in
           ty
         with Not_found ->
-          Errors.anomaly ("type_of: variable "^(Names.Id.to_string id)^" unbound"))
+          Errors.anomaly ~label:"type_of" (str "variable " ++ Names.Id.print id ++ str " unbound"))
     | T.Const c ->
         let cb = Environ.lookup_constant c env in
         Typeops.type_of_constant_type env (cb.Declarations.const_type)
@@ -212,7 +214,7 @@ let typeur sigma metamap =
     | T.Case (_,p,c,lf) ->
         let Inductiveops.IndType(_,realargs) =
           try Inductiveops.find_rectype env sigma (type_of env c)
-          with Not_found -> Errors.anomaly "type_of: Bad recursive type" in
+          with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "Bad recursive type") in
         let t = Reductionops.whd_beta sigma (T.applist (p, realargs)) in
         (match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with
           | T.Prod _ -> Reductionops.whd_beta sigma (T.applist (t, [c]))
@@ -253,7 +255,7 @@ let typeur sigma metamap =
           | _, (CProp as s) -> s)
     | T.App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
     | T.Lambda _ | T.Fix _ | T.Construct _ ->
-        Errors.anomaly "sort_of: Not a type (1)"
+        Errors.anomaly ~label:"sort_of" (Pp.str "Not a type (1)")
     | _ -> outsort env sigma (type_of env t)
 
   and sort_family_of env t =
@@ -265,7 +267,7 @@ let typeur sigma metamap =
     | T.App(f,args) ->
        sort_of_atomic_type env sigma (type_of env f) args
     | T.Lambda _ | T.Fix _ | T.Construct _ ->
-        Errors.anomaly "sort_of: Not a type (1)"
+        Errors.anomaly ~label:"sort_of" (Pp.str "Not a type (1)")
     | _ -> outsort env sigma (type_of env t)
 
   in type_of, sort_of, sort_family_of
@@ -514,7 +516,7 @@ print_endline "PASSATO" ; flush stdout ;
                add_inner_type fresh_id'' ;
               A.AEvar
                (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l))
-           | T.Meta _ -> Errors.anomaly "Meta met during exporting to XML"
+           | T.Meta _ -> Errors.anomaly (Pp.str "Meta met during exporting to XML")
            | T.Sort s -> A.ASort (fresh_id'', s)
            | T.Cast (v,_, t) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index e16f9dd19..479b04228 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -289,7 +289,7 @@ let kind_of_variable id =
     | IsAssumption Conjectural -> "VARIABLE","Conjecture"
     | IsDefinition Definition -> "VARIABLE","LocalDefinition"
     | IsProof _ -> "VARIABLE","LocalFact"
-    | _ -> Errors.anomaly "Unsupported variable kind"
+    | _ -> Errors.anomaly (Pp.str "Unsupported variable kind")
 ;;
 
 let kind_of_constant kn =
@@ -423,7 +423,7 @@ let print_ref qid fn =
 (* pretty prints via Xml.pp the proof in progress on dest     *)
 let show_pftreestate internal fn (kind,pftst) id =
  if true then
-   Errors.anomaly "Xmlcommand.show_pftreestate is not supported in this version."
+   Errors.anomaly (Pp.str "Xmlcommand.show_pftreestate is not supported in this version.")
 
 let show fn =
  let pftst = Pfedit.get_pftreestate () in
@@ -519,7 +519,7 @@ let _ =
 	  let options = " --html -s --body-only --no-index --latin1 --raw-comments" in
           let command cmd =
            if Sys.command cmd <> 0 then
-            Errors.anomaly ("Error executing \"" ^ cmd ^ "\"")
+            Errors.anomaly (Pp.str ("Error executing \"" ^ cmd ^ "\""))
           in
            command (coqdoc^options^" -o "^fn^".xml "^fn^".v");
            command ("rm "^fn^".v "^fn^".glob");