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, 23 insertions, 22 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e8e76809c6..e2d40f23fe 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -629,7 +629,7 @@ let rec extern inctx scopes vars r =
 		     | None :: q -> raise No_match
 		     | Some c :: q ->
 		         match locs with
-			   | [] -> anomaly "projections corruption [Constrextern.extern]"
+			   | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern]")
 			   | (_, false) :: locs' ->
 			       (* we don't want to print locals *)
 			       ip q locs' args acc
@@ -932,7 +932,7 @@ let rec glob_of_pat env = function
       let id = try match lookup_name_of_rel n env with
 	| Name id   -> id
 	| Anonymous ->
-	    anomaly "glob_constr_of_pattern: index to an anonymous variable"
+	    anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable")
       with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
       GVar (loc,id)
   | PMeta None -> GHole (loc,Evar_kinds.InternalHole)
@@ -960,7 +960,7 @@ let rec glob_of_pat env = function
 	| _, Some ind ->
 	  let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env c)) bl in
 	  simple_cases_matrix_of_branches ind bl'
-	| _, None -> anomaly "PCase with some branches but unknown inductive"
+	| _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive")
       in
       let mat = if info.cip_extensible then mat @ [any_any_branch] else mat
       in
@@ -968,7 +968,7 @@ let rec glob_of_pat env = function
 	| PMeta None, _, _ -> (Anonymous,None),None
 	| _, Some ind, Some nargs ->
 	  return_type_of_predicate ind nargs (glob_of_pat env p)
-	| _ -> anomaly "PCase with non-trivial predicate but unknown inductive"
+	| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive")
       in
       GCases (loc,RegularStyle,rtn,[glob_of_pat env tm,indnames],mat)
   | PFix f -> Detyping.detype false [] env (mkFix f)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 79c67165d2..2afd33babb 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -316,7 +316,7 @@ let rec it_mkGLambda loc2 env body =
 let build_impls = function
   |Implicit -> (function
 		  |Name id ->  Some (id, Impargs.Manual, (true,true))
-		  |Anonymous -> anomaly "Anonymous implicit argument")
+		  |Anonymous -> anomaly (Pp.str "Anonymous implicit argument"))
   |Explicit -> fun _ -> None
 
 let impls_type_list ?(args = []) =
@@ -543,7 +543,7 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
             (aux ((x,(a,(scopt,subscopes)))::terms,binderopt) subinfos iter))
             (if lassoc then List.rev l else l) termin
       with Not_found ->
-          anomaly "Inconsistent substitution of recursive notation")
+          anomaly (Pp.str "Inconsistent substitution of recursive notation"))
     | NHole (Evar_kinds.BinderType (Name id as na)) ->
       let na =
         try snd (coerce_to_name (fst (List.assoc id terms)))
@@ -562,7 +562,7 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
 	  termin bl in
 	make_letins letins res
       with Not_found ->
-          anomaly "Inconsistent substitution of recursive notation")
+          anomaly (Pp.str "Inconsistent substitution of recursive notation"))
     | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt ->
         let (loc,(na,bk,t)),letins = snd (Option.get binderopt) in
 	GProd (loc,na,bk,t,make_letins letins (aux subst' infos c'))
@@ -855,7 +855,7 @@ let chop_params_pattern loc ind args with_letin =
 let find_constructor loc add_params ref =
   let cstr = (function ConstructRef cstr -> cstr
     |IndRef _ -> user_err_loc (loc,"find_constructor",str "There is an inductive name deep in a \"in\" clause.")
-    |_ -> anomaly "unexpected global_reference in pattern") ref in
+    |_ -> anomaly (Pp.str "unexpected global_reference in pattern")) ref in
   cstr, (function (ind,_ as c) -> match add_params with
     |Some nb_args -> let nb = if Int.equal nb_args (Inductiveops.constructor_nrealhyps c)
       then fst (Inductiveops.inductive_nargs ind)
@@ -890,7 +890,7 @@ let sort_fields mode loc l completer =
 	      | [] -> (i, acc)
 	      | (Some name) :: b->
 		 (match m with
-		    | [] -> anomaly "Number of projections mismatch"
+		    | [] -> anomaly (Pp.str "Number of projections mismatch")
 		    | (_, regular)::tm ->
 		       let boolean = not regular in
                        begin match global_reference_of_reference refer with
@@ -914,7 +914,7 @@ let sort_fields mode loc l completer =
 	    (record.Recordops.s_EXPECTEDPARAM,
 	     Qualid (loc, shortest_qualid_of_global Id.Set.empty (ConstructRef ind)),
 	     build_patt record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 (0,[]))
-	  with Not_found -> anomaly "Environment corruption for records."
+	  with Not_found -> anomaly (Pp.str "Environment corruption for records.")
 	  in
 	(* now we want to have all fields of the pattern indexed by their place in
 	   the constructor *)
@@ -1099,7 +1099,7 @@ let drop_notations_pattern looked_for =
 	    tmp_scope = scopt} a
 	with Not_found ->
 	  if Id.equal id ldots_var then RCPatAtom (loc,Some id) else
-	    anomaly ("Unbound pattern notation variable: "^(Id.to_string id))
+	    anomaly (str "Unbound pattern notation variable: " ++ Id.print id)
       end
     | NRef g ->
       ensure_kind top g;
@@ -1122,7 +1122,7 @@ let drop_notations_pattern looked_for =
            subst_pat_iterator ldots_var t u)
            (if lassoc then List.rev l else l) termin
        with Not_found ->
-         anomaly "Inconsistent substitution of recursive notation")
+         anomaly (Pp.str "Inconsistent substitution of recursive notation"))
     | NHole _ ->
       let () = assert (List.is_empty args) in
       RCPatAtom (loc, None)
@@ -1224,7 +1224,7 @@ let get_implicit_name n imps =
 let set_hole_implicit i b = function
   | GRef (loc,r) | GApp (_,GRef (loc,r),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b))
   | GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b))
-  | _ -> anomaly "Only refs have implicits"
+  | _ -> anomaly (Pp.str "Only refs have implicits")
 
 let exists_implicit_name id =
   List.exists (fun imp -> is_status_implicit imp && Id.equal id (name_of_implicit imp))
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index a047a762bd..92a268796b 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -26,7 +26,7 @@ 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 global_of_extended_global (Nametab.extended_global_of_path sp)
-  with Not_found -> anomaly (locstr^": cannot find "^(string_of_path sp))
+  with Not_found -> anomaly ~label:locstr (str "cannot find " ++ Libnames.pr_path sp)
 
 let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
 let coq_constant locstr dir s = constr_of_global (coq_reference locstr dir s)
@@ -50,12 +50,12 @@ let gen_constant_in_modules locstr dirs s =
   match these with
     | [x] -> constr_of_global x
     | [] ->
-	anomalylabstrm "" (str (locstr^": cannot find "^s^
+	anomaly ~label:locstr (str ("cannot find "^s^
 	" in module"^(if List.length dirs > 1 then "s " else " ")) ++
 	prlist_with_sep pr_comma pr_dirpath dirs)
     | l ->
-	anomalylabstrm ""
-	(str (locstr^": found more than once object of name "^s^
+	anomaly ~label:locstr
+	(str ("found more than once object of name "^s^
 	" in module"^(if List.length dirs > 1 then "s " else " ")) ++
 	prlist_with_sep pr_comma pr_dirpath dirs)
 
@@ -183,7 +183,7 @@ let build_bool_type () =
     andb_prop =  init_constant ["Datatypes"] "andb_prop";
     andb_true_intro =  init_constant ["Datatypes"] "andb_true_intro" }
 
-let build_sigma_set () = anomaly "Use build_sigma_type"
+let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type")
 
 let build_sigma_type () =
   { proj1 = init_constant ["Specif"] "projT1";
@@ -369,7 +369,7 @@ let coq_eq_ref      = lazy (init_reference ["Logic"] "eq")
 let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
 let coq_jmeq_ref     = lazy (gen_reference "Coqlib" ["Logic";"JMeq"] "JMeq")
 let coq_eq_true_ref = lazy (gen_reference "Coqlib" ["Init";"Datatypes"] "eq_true")
-let coq_existS_ref  = lazy (anomaly "use coq_existT_ref")
+let coq_existS_ref  = lazy (anomaly (Pp.str "use coq_existT_ref"))
 let coq_existT_ref  = lazy (init_reference ["Specif"] "existT")
 let coq_exist_ref  = lazy (init_reference ["Specif"] "exist")
 let coq_not_ref     = lazy (init_reference ["Logic"] "not")
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 382c38da32..a029a3b31e 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
 open Util
 open Glob_term
 open Constrexpr
@@ -238,7 +239,7 @@ type ('a,'b) abstract_argument_type = argument_type
 
 let create_arg v s =
   if List.mem_assoc s !dyntab then
-    Errors.anomaly ("Genarg.create: already declared generic argument " ^ s);
+    Errors.anomaly ~label:"Genarg.create" (str ("already declared generic argument " ^ s));
   let t = ExtraArgType s in
   dyntab := (s,Option.map (in_gen t) v) :: !dyntab;
   (t,t,t)
diff --git a/interp/notation.ml b/interp/notation.ml
index 39a664a64a..ac71e1ebdc 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -337,7 +337,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
 
 let declare_notation_level ntn level =
   if Gmap.mem ntn !notation_level_map then
-    anomaly ("Notation "^ntn^" is already assigned a level");
+    anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level");
   notation_level_map := Gmap.add ntn level !notation_level_map
 
 let level_of_notation ntn =
@@ -887,7 +887,7 @@ let declare_notation_printing_rule ntn unpl =
 
 let find_notation_printing_rule ntn =
   try Gmap.find ntn !printing_rules
-  with Not_found -> anomaly ("No printing rule found for "^ntn)
+  with Not_found -> anomaly (str "No printing rule found for " ++ str ntn)
 
 (**********************************************************************)
 (* Synchronisation with reset *)