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, 41 insertions, 41 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 9c895e6a9c..450b3ef405 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -310,7 +310,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
 	(fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) ->
 	   try
 	     let witness = Int.Map.find i sub in
-	     if b' <> None then anomaly "can not redefine a rel!";
+	     if b' <> None then anomaly (Pp.str "can not redefine a rel!");
 	     (Termops.pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun))
 	   with Not_found  ->
 	     (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
@@ -396,7 +396,7 @@ let rewrite_until_var arg_num eq_ids : tactic =
     then tclIDTAC g
     else
       match eq_ids with
-	| [] -> anomaly "Cannot find a way to prove recursive property";
+	| [] -> anomaly (Pp.str "Cannot find a way to prove recursive property");
 	| eq_id::eq_ids ->
 	    tclTHEN
 	      (tclTRY (Equality.rewriteRL (mkVar eq_id)))
@@ -604,7 +604,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 		   observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++
 			      pr_lconstr_env (pf_env g') new_term_value_eq
 			   );
-		   anomaly "cannot compute new term value"
+		   anomaly (Pp.str "cannot compute new term value")
 	   in
 	 let fun_body =
 	   mkLambda(Anonymous,
@@ -830,7 +830,7 @@ let build_proof
 		 h_reduce_with_zeta Locusops.onConcl;
 		 build_proof do_finalize new_infos
 		] g
-	  | Rel _ -> anomaly "Free var in goal conclusion !"
+	  | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !")
   and build_proof do_finalize dyn_infos g =
 (*     observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
     observe_tac_stream (str "build_proof with " ++ Printer.pr_lconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
@@ -1014,7 +1014,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
 		{finfos with
 		   equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
 					      ConstRef c -> c
-					    | _ -> Errors.anomaly "Not a constant"
+					    | _ -> Errors.anomaly (Pp.str "Not a constant")
 					 )
 		}
 	  | _ -> ()
@@ -1208,7 +1208,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	    else
 	      h_mutual_fix this_fix_info.name (this_fix_info.idx + 1)
 		other_fix_infos
-	| _ -> anomaly "Not a valid information"
+	| _ -> anomaly (Pp.str "Not a valid information")
     in
     let first_tac : tactic = (* every operations until fix creations *)
       tclTHENSEQ
@@ -1223,7 +1223,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	let ctxt,pte_app =  (decompose_prod_assum (pf_concl gl)) in
 	let pte,pte_args = (decompose_app pte_app) in
 	try
-	  let pte = try destVar pte with _ -> anomaly "Property is not a variable"  in
+	  let pte = try destVar pte with _ -> anomaly (Pp.str "Property is not a variable")  in
 	  let fix_info = Id.Map.find  pte ptes_to_fix in
 	  let nb_args = fix_info.nb_realargs in
 	  tclTHENSEQ
@@ -1364,7 +1364,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 
 let prove_with_tcc tcc_lemma_constr eqs : tactic =
   match !tcc_lemma_constr with
-    | None -> anomaly "No tcc proof !!"
+    | None -> anomaly (Pp.str "No tcc proof !!")
     | Some lemma ->
 	fun gls ->
 (* 	  let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *)
@@ -1562,7 +1562,7 @@ let prove_principle_for_gen
   let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in
   let lemma =
     match !tcc_lemma_ref with
-     | None -> anomaly ( "No tcc proof !!")
+     | None -> anomaly (str "No tcc proof !!")
      | Some lemma -> lemma
   in
 (*   let rec list_diff del_list check_list = *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 700beaff59..9916ed95a9 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -48,7 +48,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
        let id =  Namegen.next_ident_away x avoid in
        Hashtbl.add tbl id x;
        (Name id,v,t)::(change_predicates_names (id::avoid) predicates)
-    | (Anonymous,_,_)::_ -> anomaly "Anonymous property binder "
+    | (Anonymous,_,_)::_ -> anomaly (Pp.str "Anonymous property binder ")
   in
   let avoid = (Termops.ids_of_context env_with_params ) in
   let princ_type_info =
@@ -395,7 +395,7 @@ let get_funs_constant mp dp =
 		     let const = make_con mp dp (Label.of_id id) in
 		     const,i
 		 | Anonymous ->
-		     anomaly "Anonymous fix"
+		     anomaly (Pp.str "Anonymous fix")
 	    )
 	    na
       | _ -> [|const,0|]
@@ -505,7 +505,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
   let first_type,other_princ_types =
     match l_schemes with
 	s::l_schemes -> s,l_schemes
-      | _ -> anomaly ""
+      | _ -> anomaly (Pp.str "")
   in
   let (_,(const,_,_)) =
     try
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 8acd24c883..9ec935cfdc 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1092,7 +1092,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
 		else
 		  GProd(Loc.ghost,n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
-	    | _ -> anomaly "Should not have an anonymous function here"
+	    | _ -> anomaly (Pp.str "Should not have an anonymous function here")
 		(* We have renamed all the anonymous functions during alpha_renaming phase *)
 
 	end
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index a74ae84e24..868bf58c96 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -532,7 +532,7 @@ let rec are_unifiable_aux  = function
 	     else
 	       let eqs' =
  		 try  ((List.combine cpl1 cpl2)@eqs)
-		 with _ -> anomaly "are_unifiable_aux"
+		 with _ -> anomaly (Pp.str "are_unifiable_aux")
 	       in
 	       are_unifiable_aux eqs'
 
@@ -554,7 +554,7 @@ let rec eq_cases_pattern_aux  = function
 	     else
 	       let eqs' =
  		 try  ((List.combine cpl1 cpl2)@eqs)
-		 with _ -> anomaly "eq_cases_pattern_aux"
+		 with _ -> anomaly (Pp.str "eq_cases_pattern_aux")
 	       in
 	       eq_cases_pattern_aux eqs'
 	 | _ -> raise NotUnifiable
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 6c3b009f85..850234c3bd 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -641,7 +641,7 @@ let rec add_args id new_args b =
 	    CAppExpl(Loc.ghost,(None,r),new_args)
 	| _ -> b
       end
-  | CFix  _  | CCoFix _ -> anomaly "add_args : todo"
+  | CFix  _  | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo")
   | CProdN(loc,nal,b1) ->
       CProdN(loc,
 	     List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
@@ -692,10 +692,10 @@ let rec add_args id new_args b =
       CRecord (loc,
 	       (match w with Some w -> Some (add_args id new_args w) | _ -> None),
 	       List.map (fun (e,o) -> e, add_args id new_args o) pars)
-  | CNotation _ -> anomaly "add_args : CNotation"
-  | CGeneralization _ -> anomaly "add_args : CGeneralization"
+  | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation")
+  | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization")
   | CPrim _ -> b
-  | CDelimiters _ -> anomaly "add_args : CDelimiters"
+  | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters")
 exception Stop of  Constrexpr.constr_expr
 
 
@@ -736,7 +736,7 @@ let rec chop_n_arrow n t =
 	      chop_n_arrow new_n t'
 	    with Stop t -> t
 	  end
-      | _ -> anomaly "Not enough products"
+      | _ -> anomaly (Pp.str "Not enough products")
 
 
 let rec get_args b t : Constrexpr.local_binder list *
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index dfbfdce3a3..a041205bf5 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -389,7 +389,7 @@ let _ =
 
 let find_or_none id =
   try Some
-    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly "Not a constant"
+    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly (Pp.str "Not a constant")
     )
   with Not_found -> None
 
@@ -417,7 +417,7 @@ let add_Function is_general f =
   and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
   and graph_ind =
     match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
-    with | IndRef ind -> ind | _ -> Errors.anomaly "Not an inductive"
+    with | IndRef ind -> ind | _ -> Errors.anomaly (Pp.str "Not an inductive")
   in
   let finfos =
     { function_constant = f;
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index eed4211590..a061cfaca7 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -112,7 +112,7 @@ let generate_type g_to_f f graph i =
   let ctxt,_ = decompose_prod_assum graph_arity in
   let fun_ctxt,res_type =
     match ctxt with
-      | [] | [_] -> anomaly "Not a valid context"
+      | [] | [_] -> anomaly (Pp.str "Not a valid context")
       | (_,_,res_type)::fun_ctxt -> fun_ctxt,res_type
   in
   let rec args_from_decl i accu = function
@@ -277,7 +277,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	(fun (_,pat) acc ->
 	     match pat with
 	       | Genarg.IntroIdentifier id -> Id.Set.add id acc
-	| _ -> anomaly "Not an identifier"
+	| _ -> anomaly (Pp.str "Not an identifier")
 	)
 	(List.nth intro_pats (pred i))
 	Id.Set.empty
@@ -316,7 +316,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       	  (fun (_,pat) acc ->
       	     match pat with
 	       | IntroIdentifier id -> id::acc
-      	       | _ -> anomaly "Not an identifier"
+      	       | _ -> anomaly (Pp.str "Not an identifier")
       	  )
       	  (List.nth intro_pats (pred i))
       	  []
@@ -423,7 +423,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       Array.map
 	(fun (_,(ctxt,concl)) ->
 	   match ctxt with
-	     | [] | [_] | [_;_] -> anomaly "bad context"
+	     | [] | [_] | [_;_] -> anomaly (Pp.str "bad context")
 	     | hres::res::(x,_,t)::ctxt ->
 		 Termops.it_mkLambda_or_LetIn
 		   (Termops.it_mkProd_or_LetIn concl [hres;res])
@@ -488,7 +488,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       Array.map
 	(fun (_,(ctxt,concl)) ->
 	   match ctxt with
-	     | [] | [_] | [_;_] -> anomaly "bad context"
+	     | [] | [_] | [_;_] -> anomaly (Pp.str "bad context")
 	     | hres::res::(x,_,t)::ctxt ->
 		 Termops.it_mkLambda_or_LetIn
 		   (Termops.it_mkProd_or_LetIn concl [hres;res])
@@ -541,7 +541,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	  (fun (_,pat) acc ->
 	     match pat with
 	       | Genarg.IntroIdentifier id -> Id.Set.add id acc
-	       | _ -> anomaly "Not an identifier"
+	       | _ -> anomaly (Pp.str "Not an identifier")
 	  )
 	  (List.nth intro_pats (pred i))
 	  Id.Set.empty
@@ -935,7 +935,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
       then
 	let eq_lemma =
 	  try Option.get (infos).equation_lemma
-	  with Option.IsNone -> anomaly "Cannot find equation lemma"
+	  with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma")
 	in
 	tclTHENSEQ[
 	  tclMAP h_intro ids;
@@ -1146,7 +1146,7 @@ let revert_graph kn post_tac hid g =
 	    let info =
 	      try find_Function_of_graph ind'
 	      with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*)
-		anomaly "Cannot retrieve infos about a mutual block"
+		anomaly (Pp.str "Cannot retrieve infos about a mutual block")
 	    in
 	    (* if we can find a completeness lemma for this function
 	       then we can come back to the functional form. If not, we do nothing
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 4b87a9b9cc..8816d960f9 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -73,8 +73,8 @@ let def_of_const t =
              | Some c -> Declarations.force c
 	     | _ -> assert false)
        with _ ->
-	 anomaly ("Cannot find definition of constant "^
-		    (Id.to_string (Label.to_id (con_label sp))))
+	 anomaly (str "Cannot find definition of constant " ++
+		    (Id.print (Label.to_id (con_label sp))))
       )
      |_ -> assert false
 
@@ -91,7 +91,7 @@ let constant sl s =
 	       (Id.of_string s)));;
 let const_of_ref = function
     ConstRef kn -> kn
-  | _ -> anomaly "ConstRef expected"
+  | _ -> anomaly (Pp.str "ConstRef expected")
 
 
 let nf_zeta env =
@@ -426,7 +426,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	travel jinfo new_continuation_tac 
 	  {expr_info with info = b; is_final=false}
       end
-    | Rel _ -> anomaly "Free var in goal conclusion !"
+    | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !")
     | Prod _ -> 
       begin
 	try
@@ -1115,7 +1115,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
       let f_id =
 	match f_name with
 	  | Name f_id -> next_ident_away_in_goal f_id ids
-	  | Anonymous -> anomaly "Anonymous function"
+	  | Anonymous -> anomaly (Pp.str "Anonymous function")
       in
       let n_names_types,_ = decompose_lam_n nb_args body1 in
       let n_ids,ids =
@@ -1125,7 +1125,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
 	       | Name id ->
 		   let n_id = next_ident_away_in_goal id ids in
 		   n_id::n_ids,n_id::ids
-	       | _ -> anomaly "anonymous argument"
+	       | _ -> anomaly (Pp.str "anonymous argument")
 	  )
 	  ([],(f_id::ids))
 	  n_names_types
@@ -1249,7 +1249,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     | Some s -> s
     | None   ->
 	try (add_suffix current_proof_name "_subproof")
-	with _ -> anomaly "open_new_goal with an unamed theorem"
+	with _ -> anomaly (Pp.str "open_new_goal with an unamed theorem")
   in
   let sign = initialize_named_context_for_proof () in
   let na = next_global_ident_away name [] in
@@ -1261,7 +1261,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
       let na_global = Nametab.global na_ref in
       match na_global with
 	  ConstRef c -> is_opaque_constant c
-	| _ -> anomaly "equation_lemma: not a constant"
+	| _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant")
     in
     let lemma = mkConst (Lib.make_con na) in
     ref_ := Some lemma ;
@@ -1405,7 +1405,7 @@ let (com_eqn : int -> Id.t ->
     let opacity =
       match terminate_ref with
 	| ConstRef c -> is_opaque_constant c
-	| _ -> anomaly "terminate_lemma: not a constant"
+	| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant")
     in
     let (evmap, env) = Lemmas.get_current_context() in
     let f_constr = constr_of_global f_ref in
@@ -1499,7 +1499,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
 	begin
 	  if do_observe ()
 	  then msg_debug (str "Cannot create equation Lemma " ++ Errors.print e)
-	  else anomaly "Cannot create equation Lemma"
+	  else anomaly (Pp.str "Cannot create equation Lemma")
 	  ;
 	  true
 	end
@@ -1533,7 +1533,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   with e ->
     begin
       (try ignore (Backtrack.backto previous_label) with _ -> ());
-      (*       anomaly "Cannot create termination Lemma" *)
+      (*       anomaly (Pp.str "Cannot create termination Lemma") *)
       raise e
     end