Uniformization of the "anomaly" command.

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

11 files changed, 34 insertions, 34 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index f251b4f85..0ab86cb04 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -557,7 +557,7 @@ let make_resolve_hyp env sigma (hname,_,htyp) =
        (mkVar hname, htyp)]
   with
     | Failure _ -> []
-    | e when Logic.catchable_exception e -> anomaly "make_resolve_hyp"
+    | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp")
 
 (* REM : in most cases hintname = id *)
 let make_unfold eref =
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 27d086095..f86c22bcf 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -563,7 +563,7 @@ let fix_r2l_forward_rew_scheme c =
 	      (Reductionops.whd_beta Evd.empty
 		(applist (c,
 	          extended_rel_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))
-  | _ -> anomaly "Ill-formed non-dependent left-to-right rewriting scheme"
+  | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme")
 
 (**********************************************************************)
 (* Build the right-to-left rewriting lemma for conclusion associated  *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7ca1116ba..226f0c20f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -946,7 +946,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
     else
       let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with
 	| (_sigS,[a;p]) -> (a,p)
- 	| _ -> anomaly "sig_clausal_form: should be a sigma type" in
+ 	| _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type") in
       let ev = Evarutil.e_new_evar evdref env a in
       let rty = beta_applist(p_i_minus_1,[ev]) in
       let tuple_tail = sigrec_clausal_form (siglen-1) rty in
@@ -960,7 +960,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
               applist(exist_term,[w_type;p_i_minus_1;w;tuple_tail])
             else
               error "Cannot solve a unification problem."
-	| None -> anomaly "Not enough components to build the dependent tuple"
+	| None -> anomaly (Pp.str "Not enough components to build the dependent tuple")
   in
   let scf = sigrec_clausal_form siglen ty in
   Evarutil.nf_evar !evdref scf
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 2cfec1e21..f802788d4 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -583,7 +583,7 @@ let subst_hole_with_term occ tc t =
 open Tacmach
 
 let out_arg = function
-  | ArgVar _ -> anomaly "Unevaluated or_var variable"
+  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
   | ArgArg x -> x
 
 let hResolve id c occ t gl = 
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index b873c2050..9adb237a9 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -289,7 +289,7 @@ let match_arrow_pattern t =
   match matches coq_arrow_pattern t with
     | [(m1,arg);(m2,mind)] ->
       assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind)
-    | _ -> anomaly "Incorrect pattern matching"
+    | _ -> anomaly (Pp.str "Incorrect pattern matching")
 
 let match_with_nottype t =
   try
@@ -373,7 +373,7 @@ let match_eq eqn eq_pat =
     | [(m1,t);(m2,x);(m3,t');(m4,x')] ->
         assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3 && Id.equal m4 meta4);
 	HeterogenousEq (t,x,t',x')
-    | _ -> anomaly "match_eq: an eq pattern should match 3 or 4 terms"
+    | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 or 4 terms")
 
 let equalities =
   [coq_eq_pattern, build_coq_eq_data;
@@ -414,7 +414,7 @@ let match_eq_nf gls eqn eq_pat =
     | [(m1,t);(m2,x);(m3,y)] ->
         assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
 	(t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y)
-    | _ -> anomaly "match_eq: an eq pattern should match 3 terms"
+    | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms")
 
 let dest_nf_eq gls eqn =
   try
@@ -435,7 +435,7 @@ let match_sigma ex ex_pat =
         assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3 && Id.equal m4 meta4);
 	(a,p,car,cdr)
     | _ ->
-	anomaly "match_sigma: a successful sigma pattern should match 4 terms"
+	anomaly ~label:"match_sigma" (Pp.str "a successful sigma pattern should match 4 terms")
 
 let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *)
   first_match (match_sigma ex)
@@ -448,7 +448,7 @@ let coq_sig_pattern = lazy PATTERN [ %coq_sig_ref ?X1 ?X2 ]
 let match_sigma t =
   match matches (Lazy.force coq_sig_pattern) t with
     | [(_,a); (_,p)] -> (a,p)
-    | _ -> anomaly "Unexpected pattern"
+    | _ -> anomaly (Pp.str "Unexpected pattern")
 
 let is_matching_sigma t = is_matching (Lazy.force coq_sig_pattern) t
 
@@ -486,7 +486,7 @@ let match_eqdec t =
   match subst with
   | [(_,typ);(_,c1);(_,c2)] ->
       eqonleft, Globnames.constr_of_global (Lazy.force op), c1, c2, typ
-  | _ -> anomaly "Unexpected pattern"
+  | _ -> anomaly (Pp.str "Unexpected pattern")
 
 (* Patterns "~ ?" and "? -> False" *)
 let coq_not_pattern = lazy PATTERN [ ~ _ ]
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 811ee03c7..cc4b9d392 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -167,7 +167,7 @@ let build_signature evars env m (cstrs : (types * types option) option list)
 	    let arg' = mkApp (Lazy.force forall_relation, [| ty ; pred ; liftarg |]) in
 	      if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
 	      else error "build_signature: no constraint can apply on a dependent argument"
-      | _, obj :: _ -> anomaly "build_signature: not enough products"
+      | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products")
       | _, [] ->
 	  (match finalcstr with
 	  | None | Some (_, None) ->
@@ -1440,7 +1440,7 @@ let rec strategy_of_ast = function
       | "try" -> Strategies.try_
       | "any" -> Strategies.any
       | "repeat" -> Strategies.repeat
-      | _ -> anomalylabstrm "strategy_of_ast" (str"Unkwnon strategy: " ++ str f)
+      | _ -> anomaly ~label:"strategy_of_ast" (str"Unkwnon strategy: " ++ str f)
     in f' s'
   | StratBinary (f, s, t) ->
     let s' = strategy_of_ast s in
@@ -1448,7 +1448,7 @@ let rec strategy_of_ast = function
     let f' = match f with
       | "compose" -> Strategies.seq
       | "choice" -> Strategies.choice
-      | _ -> anomalylabstrm "strategy_of_ast" (str"Unkwnon strategy: " ++ str f)
+      | _ -> anomaly ~label:"strategy_of_ast" (str"Unkwnon strategy: " ++ str f)
     in f' s' t'
   | StratConstr (c, b) -> apply_glob_constr (fst c) b AllOccurrences
   | StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 8fbab3ca1..d3c9e6bb6 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -773,8 +773,8 @@ and intern_tacarg strict onlytac ist = function
       (match Dyn.tag t with
 	| "tactic" | "value" -> x
         | "constr" -> if onlytac then error_tactic_expected loc else x
-	| s -> anomaly_loc (loc, "",
-                 str "Unknown dynamic: <" ++ str s ++ str ">"))
+	| s -> anomaly ~loc
+                 (str "Unknown dynamic: <" ++ str s ++ str ">"))
 
 (* Reads the rules of a Match Context or a Match *)
 and intern_match_rule onlytac ist = function
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 7a041214d..730be9303 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -234,7 +234,7 @@ let try_interp_ltac_var coerce ist env (loc,id) =
 
 let interp_ltac_var coerce ist env locid =
   try try_interp_ltac_var coerce ist env locid
-  with Not_found -> anomaly ("Detected '" ^ (Id.to_string (snd locid)) ^ "' as ltac var at interning time")
+  with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time")
 
 (* Interprets an identifier which must be fresh *)
 let coerce_to_ident fresh env = function
@@ -1121,8 +1121,8 @@ and interp_tacarg ist gl arg =
 	else if String.equal tg "constr" then
         VConstr ([],constr_out t)
 	else
-          anomaly_loc (dloc, "Tacinterp.val_interp",
-		       (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">"))
+          anomaly ~loc:dloc ~label:"Tacinterp.val_interp"
+		       (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">")
   in
   !evdref , v
 
@@ -1964,7 +1964,7 @@ let globTacticIn t = TacArg (dloc,TacDynamic (dloc,tactic_in t))
 let tacticIn t =
   globTacticIn (fun ist ->
     try glob_tactic (t ist)
-    with e -> anomalylabstrm "tacticIn"
+    with e -> anomaly ~label:"tacticIn"
       (str "Incorrect tactic expression. Received exception is:" ++
        Errors.print e))
 
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index d2d6de623..90739a4e9 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -284,8 +284,8 @@ and subst_tacarg subst = function
 	| "tactic" | "value" -> x
         | "constr" ->
           TacDynamic(the_loc, constr_in (subst_mps subst (constr_out t)))
-	| s -> Errors.anomaly_loc (dloc, "Tacinterp.val_interp",
-                 str "Unknown dynamic: <" ++ str s ++ str ">"))
+	| s -> Errors.anomaly ~loc:dloc ~label:"Tacinterp.val_interp"
+                 (str "Unknown dynamic: <" ++ str s ++ str ">"))
 
 (* Reads the rules of a Match Context or a Match *)
 and subst_match_rule subst = function
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 9b32f108c..f7a8a787c 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -207,7 +207,7 @@ let compute_construtor_signatures isrec (_,k as ity) =
 	in b :: (analrec c rest)
     | LetIn (_,_,_,c), rest -> false :: (analrec c rest)
     | _, [] -> []
-    | _ -> anomaly "compute_construtor_signatures"
+    | _ -> anomaly (Pp.str "compute_construtor_signatures")
   in
   let (mib,mip) = Global.lookup_inductive ity in
   let n = mib.mind_nparams in
@@ -239,7 +239,7 @@ let general_elim_then_using mk_elim
   let indmv =
     match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
       | Meta mv -> mv
-      | _         -> anomaly "elimination"
+      | _         -> anomaly (Pp.str "elimination")
   in
   let pmv =
     let p, _ = decompose_app elimclause.templtyp.Evd.rebus in
@@ -335,11 +335,11 @@ let make_elim_branch_assumptions ba gl =
 		   id::constargs,
 		   recargs,
 		   indargs) tl idtl
-      | (_, _) -> anomaly "make_elim_branch_assumptions"
+      | (_, _) -> anomaly (Pp.str "make_elim_branch_assumptions")
   in
   makerec ([],[],[],[],[]) ba.branchsign
     (try List.firstn ba.nassums (pf_hyps gl)
-     with Failure _ -> anomaly "make_elim_branch_assumptions")
+     with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions"))
 
 let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl
 
@@ -359,11 +359,11 @@ let make_case_branch_assumptions ba gl =
 		   id::cargs,
 		   recargs,
 		   id::constargs) tl idtl
-      | (_, _) -> anomaly "make_case_branch_assumptions"
+      | (_, _) -> anomaly (Pp.str "make_case_branch_assumptions")
   in
   makerec ([],[],[],[]) ba.branchsign
     (try List.firstn ba.nassums (pf_hyps gl)
-     with Failure _ -> anomaly "make_case_branch_assumptions")
+     with Failure _ -> anomaly (Pp.str "make_case_branch_assumptions"))
 
 let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c769fb3ba..6ba5e0e04 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -692,7 +692,7 @@ let cut_in_parallel l =
 
 let error_uninstantiated_metas t clenv =
   let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
-  let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta"
+  let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta")
   in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
 
 (* For a clenv expressing some lemma [C[?1:T1,...,?n:Tn] : P] and some
@@ -724,13 +724,13 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id c
 let last_arg c = match kind_of_term c with
   | App (f,cl) ->
       Array.last cl
-  | _ -> anomaly "last_arg"
+  | _ -> anomaly (Pp.str "last_arg")
 
 let nth_arg i c =
   if Int.equal i (-1) then last_arg c else
   match kind_of_term c with
   | App (f,cl) -> cl.(i)
-  | _ -> anomaly "nth_arg"
+  | _ -> anomaly (Pp.str "nth_arg")
 
 let index_of_ind_arg t =
   let rec aux i j t = match kind_of_term t with
@@ -1630,7 +1630,7 @@ let quantify lconstr =
 *)
 
 let out_arg = function
-  | ArgVar _ -> anomaly "Unevaluated or_var variable"
+  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
   | ArgArg x -> x
 
 let occurrences_of_hyp id cls =
@@ -2998,7 +2998,7 @@ let induction_from_context_l with_evars elim_info lid names gl =
      context. *)
   let hyp0,indvars,lid_params =
     match lid with
-      | []  -> anomaly "induction_from_context_l"
+      | []  -> anomaly (Pp.str "induction_from_context_l")
       | e::l ->
 	  let nargs_without_first = nargs_indarg_farg - 1 in
 	  let ivs,lp = cut_list nargs_without_first l in
@@ -3272,7 +3272,7 @@ let elim_scheme_type elim t gl =
 	  clenv_unify ~flags:elim_flags Reduction.CUMUL t
             (clenv_meta_type clause mv) clause in
 	res_pf clause' ~flags:elim_flags gl
-    | _ -> anomaly "elim_scheme_type"
+    | _ -> anomaly (Pp.str "elim_scheme_type")
 
 let elim_type t gl =
   let (ind,t) = pf_reduce_to_atomic_ind gl t in