Uniformization of the "anomaly" command.

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

5 files changed, 9 insertions, 9 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index ebb1cbcd4..158f8e94f 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -167,7 +167,7 @@ let error_incompatible_inst clenv mv  =
           (str "An incompatible instantiation has already been found for " ++
            pr_id id)
     | _ ->
-        anomaly "clenv_assign: non dependent metavar already assigned"
+        anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned")
 
 (* TODO: replace by clenv_unify (mkMeta mv) rhs ? *)
 let clenv_assign mv rhs clenv =
@@ -421,7 +421,7 @@ let error_already_defined b =
           (str "Binder name \"" ++ pr_id id ++
            str"\" already defined with incompatible value.")
     | AnonHyp n ->
-        anomalylabstrm ""
+        anomaly
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 38e536ba2..a9aa4fa59 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -63,7 +63,7 @@ let rec advance sigma g =
     let v =
       match evi.Evd.evar_body with
       | Evd.Evar_defined c -> c
-      | _ -> Errors.anomaly "Some goal is marked as 'cleared' but is uninstantiated"
+      | _ -> Errors.anomaly (Pp.str "Some goal is marked as 'cleared' but is uninstantiated")
     in
     let (e,_) = Term.destEvar v in
     let g' = { g with content = e } in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 45ef3efad..2f88c79a7 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -386,7 +386,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 
     | _ ->
 	if occur_meta trm then
-	  anomaly "refiner called with a meta in non app/case subterm";
+	  anomaly (Pp.str "refiner called with a meta in non app/case subterm");
 
       	let t'ty = goal_type_of env sigma trm in
 	check_conv_leq_goal env sigma trm t'ty conclty;
@@ -434,7 +434,7 @@ and mk_hdgoals sigma goal goalacc trm =
 
     | _ ->
 	if !check && occur_meta trm then
-	  anomaly "refine called with a dependent meta";
+	  anomaly (Pp.str "refine called with a dependent meta");
 	goalacc, goal_type_of env sigma trm, sigma, trm
 
 and mk_arggoals sigma goal goalacc funty = function
@@ -457,7 +457,7 @@ and mk_casegoals sigma goal goalacc p c =
   let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in
   let indspec =
     try Tacred.find_hnf_rectype env sigma ct
-    with Not_found -> anomaly "mk_casegoals" in
+    with Not_found -> anomaly (Pp.str "mk_casegoals") in
   let (lbrty,conclty) =
     type_case_branches_with_names env indspec p c in
   (acc'',lbrty,conclty,sigma,p',c')
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index ad334e91c..ef92e8e42 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -64,7 +64,7 @@ let cook_proof hook =
   hook prf;
   match Proof_global.close_proof () with
   | (i,([e],cg,str,h)) -> (i,(e,cg,str,h))
-  | _ -> Errors.anomaly "Pfedit.cook_proof: more than one proof term."
+  | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
 
 let xml_cook_proof = ref (fun _ -> ())
 let set_xml_cook_proof f = xml_cook_proof := f
@@ -113,7 +113,7 @@ let get_current_goal_context () =
 let current_proof_statement () =
   match Proof_global.V82.get_current_initial_conclusions () with
     | (id,([concl],strength,hook)) -> id,strength,concl,hook
-    | _ -> Errors.anomaly "Pfedit.current_proof_statement: more than one statement"
+    | _ -> Errors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement")
 
 let solve_nth ?(with_end_tac=false) gi tac = 
   try 
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index b57ee2118..828da8688 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -170,7 +170,7 @@ let decl_red_expr s e =
   end
 
 let out_arg = function
-  | ArgVar _ -> anomaly "Unevaluated or_var variable"
+  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
   | ArgArg x -> x
 
 let out_with_occurrences (occs,c) =