Uniformization of the "anomaly" command.

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

8 files changed, 26 insertions, 24 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 49fe6d0ba..18640d9d4 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -153,7 +153,7 @@ let find_logical_path phys_dir =
   match List.filter2 (fun p d -> p = phys_dir) physical logical with
   | _,[dir] -> dir
   | _,[] -> default_root_prefix
-  | _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
+  | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir))
 
 let remove_load_path dir =
   let physical, logical = !load_paths in
@@ -185,7 +185,7 @@ let add_load_path (phys_path,coq_path) =
 	    end
       | _,[] ->
 	  load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
-      | _ -> anomaly ("Two logical paths are associated to "^phys_path)
+      | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path))
 
 let load_paths_of_dir_path dir =
   let physical, logical = !load_paths in
diff --git a/checker/environ.ml b/checker/environ.ml
index a0fac3492..0b475ad49 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -111,9 +111,11 @@ let add_constraints c env =
 let lookup_constant kn env =
   Cmap_env.find kn env.env_globals.env_constants
 
+let anomaly s = anomaly (Pp.str s)
+
 let add_constant kn cs env =
   if Cmap_env.mem kn env.env_globals.env_constants then
-    Printf.ksprintf anomaly "Constant %s is already defined"
+    Printf.ksprintf anomaly ("Constant %s is already defined")
       (string_of_con kn);
   let new_constants =
     Cmap_env.add kn cs env.env_globals.env_constants in
@@ -155,7 +157,7 @@ let lookup_mind kn env =
 
 let add_mind kn mib env =
   if Mindmap_env.mem kn env.env_globals.env_inductives then
-    Printf.ksprintf anomaly "Inductive %s is already defined"
+    Printf.ksprintf anomaly ("Inductive %s is already defined")
       (string_of_mind kn);
   let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
   let kn1,kn2 =  user_mind kn,canonical_mind kn in
@@ -174,7 +176,7 @@ let add_mind kn mib env =
 
 let add_modtype ln mtb env =
   if MPmap.mem ln env.env_globals.env_modtypes then
-    Printf.ksprintf anomaly "Module type %s is already defined"
+    Printf.ksprintf anomaly ("Module type %s is already defined")
       (string_of_mp ln);
   let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in
   let new_globals =
@@ -184,7 +186,7 @@ let add_modtype ln mtb env =
 
 let shallow_add_module mp mb env =
   if MPmap.mem mp env.env_globals.env_modules then
-    Printf.ksprintf anomaly "Module %s is already defined"
+    Printf.ksprintf anomaly ("Module %s is already defined")
       (string_of_mp mp);
   let new_mods = MPmap.add mp mb env.env_globals.env_modules in
   let new_globals =
@@ -194,7 +196,7 @@ let shallow_add_module mp mb env =
 
 let shallow_remove_module mp env =
   if not (MPmap.mem mp env.env_globals.env_modules) then
-    Printf.ksprintf anomaly "Module %s is unknown"
+    Printf.ksprintf anomaly ("Module %s is unknown")
       (string_of_mp mp);
   let new_mods = MPmap.remove mp env.env_globals.env_modules in
   let new_globals =
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 285be1bc9..8b56b5365 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -100,7 +100,7 @@ let rec sorts_of_constr_args env t =
         let env1 = push_rel (name,Some def,ty) env in
 	sorts_of_constr_args env1 c
     | _ when is_constructor_head t -> []
-    | _ -> anomaly "infos_and_sort: not a positive constructor"
+    | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor")
 
 
 (* Prop and Set are small *)
@@ -299,11 +299,11 @@ let failwith_non_pos n ntypes c =
 
 let failwith_non_pos_vect n ntypes v =
   Array.iter (failwith_non_pos n ntypes) v;
-  anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur"
+  anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur")
 
 let failwith_non_pos_list n ntypes l =
   List.iter (failwith_non_pos n ntypes) l;
-  anomaly "failwith_non_pos_list: some k in [n;n+ntypes-1] should occur"
+  anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur")
 
 (* Conclusion of constructors: check the inductive type is called with
    the expected parameters *)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index b04c77ad8..abc162af7 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -67,7 +67,7 @@ let constructor_instantiate mind mib c =
 
 let instantiate_params full t args sign =
   let fail () =
-    anomaly "instantiate_params: type, ctxt and args mismatch" in
+    anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
   let (rem_args, subs, ty) =
     fold_rel_context
       (fun (_,copt,_) (largs,subs,ty) ->
@@ -778,7 +778,7 @@ let check_one_fix renv recpos def =
 	    check_rec_call renv [] a;
             let renv' = push_var_renv renv (x,a) in
 	      check_nested_fix_body renv' (decr-1) recArgsDecrArg b
-	| _ -> anomaly "Not enough abstractions in fix body"
+	| _ -> anomaly (Pp.str "Not enough abstractions in fix body")
 	    
   in
   check_rec_call renv [] def
@@ -792,7 +792,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
     or Array.length names <> nbfix
     or bodynum < 0
     or bodynum >= nbfix
-  then anomaly "Ill-formed fix term";
+  then anomaly (Pp.str "Ill-formed fix term");
   let fixenv = push_rec_types recdef env in
   let raise_err env i err =
     error_ill_formed_rec_body env err names i in
@@ -813,7 +813,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
 		    raise_err env i (RecursionNotOnInductiveType a) in
                 (mind, (env', b))
 	      else check_occur env' (n+1) b
-            else anomaly "check_one_fix: Bad occurrence of recursive call"
+            else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call")
         | _ -> raise_err env i NotEnoughAbstractionInFixBody in
     check_occur fixenv 1 def in
   (* Do it on every fixpoint *)
@@ -842,7 +842,7 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
 exception CoFixGuardError of env * guard_error
 
 let anomaly_ill_typed () =
-  anomaly "check_one_cofix: too many arguments applied to constructor"
+  anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor")
 
 let rec codomain_is_coind env c =
   let b = whd_betadeltaiota env c in
diff --git a/checker/modops.ml b/checker/modops.ml
index f9c52c2e9..6b7a9c7a1 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -90,7 +90,7 @@ and add_module mb env =
       | SEBstruct (sign) -> 
 	    add_signature mp sign mb.mod_delta env
       | SEBfunctor _ -> env
-      | _ -> anomaly "Modops:the evaluation of the structure failed "
+      | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
 
 
 let strengthen_const mp_from l cb resolver =
@@ -118,7 +118,7 @@ let rec strengthen_mod mp_from mp_to mb =
 	       (add_delta_resolver mb.mod_delta resolve_out)*);
 	       mod_retroknowledge = mb.mod_retroknowledge}
      | SEBfunctor _ -> mb
-     | _ -> anomaly "Modops:the evaluation of the structure failed "
+     | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
 	 
 and strengthen_sig mp_from sign mp_to resolver =
   match sign with
@@ -152,7 +152,7 @@ let strengthen mtb mp =
 	       typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
 		(add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)}
       | SEBfunctor _ -> mtb
-      | _ -> anomaly "Modops:the evaluation of the structure failed "
+      | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
 
 let subst_and_strengthen mb mp =
   strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index c2d5c261c..57e39f9ce 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -287,13 +287,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
     (* Eta-expansion on the fly *)
     | (FLambda _, _) ->
         if v1 <> [] then
-          anomaly "conversion was given unreduced term (FLambda)";
+          anomaly (Pp.str "conversion was given unreduced term (FLambda)");
         let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
         eqappr univ CONV infos
           (el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2))
     | (_, FLambda _) ->
         if v2 <> [] then
-          anomaly "conversion was given unreduced term (FLambda)";
+          anomaly (Pp.str "conversion was given unreduced term (FLambda)");
         let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
         eqappr univ CONV infos
           (el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[]))
@@ -398,7 +398,7 @@ let vm_conv = fconv
 let hnf_prod_app env t n =
   match whd_betadeltaiota env t with
     | Prod (_,_,b) -> subst1 n b
-    | _ -> anomaly "hnf_prod_app: Need a product"
+    | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
 
 let hnf_prod_applist env t nl =
   List.fold_left (hnf_prod_app env) t nl
diff --git a/checker/term.ml b/checker/term.ml
index 6bafeda7f..e7e9c891b 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -441,7 +441,7 @@ let destArity =
     | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c
     | Cast (c,_,_)    -> prodec_rec l c
     | Sort s          -> l,s
-    | _               -> anomaly "destArity: not an arity"
+    | _               -> anomaly ~label:"destArity" (Pp.str "not an arity")
   in
   prodec_rec []
 
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 129c242b9..07c7bc367 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -351,10 +351,10 @@ let rec execute env cstr =
 
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
-	anomaly "the kernel does not support metavariables"
+	anomaly (Pp.str "the kernel does not support metavariables")
 
     | Evar _ ->
-	anomaly "the kernel does not support existential variables"
+	anomaly (Pp.str "the kernel does not support existential variables")
 
 and execute_type env constr =
   let j = execute env constr in