From 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 28 Jan 2013 21:05:35 +0000
Subject: Uniformization of the "anomaly" command.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/decl_mode/ppdecl_proof.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/decl_mode/ppdecl_proof.ml')

diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index 01f32e4a32..7f63c4200d 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 () ++
-- 
cgit v1.2.3