Uniformization of the "anomaly" command.

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

4 files changed, 10 insertions, 10 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 9f6715a7d9..4c0771aefa 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -123,7 +123,7 @@ let pr_expl_args pr (a,expl) =
   match expl with
   | None -> pr (lapp,L) a
   | Some (_,ExplByPos (n,_id)) ->
-      anomaly("Explicitation by position not implemented")
+      anomaly (Pp.str "Explicitation by position not implemented")
   | Some (_,ExplByName id) ->
       str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
 
@@ -242,7 +242,7 @@ let pr_binder many pr (nal,k,t) =
 	  hov 1 (str "`" ++ (surround_impl b'
 			       (pr_lident (loc,id) ++ str " : " ++
 				  (if t' then str "!" else mt()) ++ pr t)))
-	|_ -> anomaly "List of generalized binders have alwais one element."
+	|_ -> anomaly (Pp.str "List of generalized binders have alwais one element.")
       end
     | Default b ->
       match t with
@@ -305,7 +305,7 @@ let split_lambda = function
   | CLambdaN (loc,[[na],bk,t],c) -> (na,t,c)
   | CLambdaN (loc,([na],bk,t)::bl,c) -> (na,t,CLambdaN(loc,bl,c))
   | CLambdaN (loc,(na::nal,bk,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,bk,t)::bl,c))
-  | _ -> anomaly "ill-formed fixpoint body"
+  | _ -> anomaly (Pp.str "ill-formed fixpoint body")
 
 let rename na na' t c =
   match (na,na') with
@@ -318,7 +318,7 @@ let split_product na' = function
   | CProdN (loc,([na],bk,t)::bl,c) -> rename na na' t (CProdN(loc,bl,c))
   | CProdN (loc,(na::nal,bk,t)::bl,c) ->
       rename na na' t (CProdN(loc,(nal,bk,t)::bl,c))
-  | _ -> anomaly "ill-formed fixpoint body"
+  | _ -> anomaly (Pp.str "ill-formed fixpoint body")
 
 let rec split_fix n typ def =
   if Int.equal n 0 then ([],typ,def)
@@ -363,7 +363,7 @@ let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) =
   pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c
 
 let pr_recursive pr_decl id = function
-  | [] -> anomaly "(co)fixpoint with no definition"
+  | [] -> anomaly (Pp.str "(co)fixpoint with no definition")
   | [d1] -> pr_decl false d1
   | dl ->
       prlist_with_sep (fun () -> fnl() ++ str "with ")
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 5a53968755..14fae2612f 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -502,7 +502,7 @@ let pr_let_clauses recflag pr = function
       hv 0
         (pr_let_clause (if recflag then "let rec " else "let ") pr hd ++
          prlist (fun t -> spc () ++ pr_let_clause "with " pr t) tl)
-  | [] -> anomaly "LetIn must declare at least one binding"
+  | [] -> anomaly (Pp.str "LetIn must declare at least one binding")
 
 let pr_seq_body pr tl =
   hv 0 (str "[ " ++
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index b78e73e486..c04b99c5d9 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -151,7 +151,7 @@ let pr_section_locality local =
 
 let pr_explanation (e,b,f) =
   let a = match e with
-  | ExplByPos (n,_) -> anomaly "No more supported"
+  | ExplByPos (n,_) -> anomaly (Pp.str "No more supported")
   | ExplByName id -> pr_id id in
   let a = if f then str"!" ++ a else a in
     if b then str "[" ++ a ++ str "]" else a
@@ -336,7 +336,7 @@ let pr_assumption_token many = function
       str (if many then "Parameters" else "Parameter")
   | (Global,Conjectural) -> str"Conjecture"
   | (Local,Conjectural) ->
-      anomaly "Don't know how to beautify a local conjecture"
+      anomaly (Pp.str "Don't know how to beautify a local conjecture")
 
 let pr_params pr_c (xl,(c,t)) =
   hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++
@@ -963,7 +963,7 @@ and pr_extend s cl =
       match rl with
       | Egramml.GramTerminal s :: rl -> str s, rl, cl
       | Egramml.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl
-      | [] -> anomaly "Empty entry" in
+      | [] -> anomaly (Pp.str "Empty entry") in
     let (pp,_) =
       List.fold_left
         (fun (strm,args) pi ->
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 2b0f458c1e..5980dae0cd 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -203,7 +203,7 @@ let rec print_modexpr env mp locals mexpr = match mexpr with
   | SEBapply _ ->
       let lapp = flatten_app mexpr [] in
       hov 3 (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")")
-  | SEBwith (_,_)-> anomaly "Not available yet"
+  | SEBwith (_,_)-> anomaly (Pp.str "Not available yet")
 
 
 let rec printable_body dir =