From 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Aug 2016 01:58:04 +0200
Subject: Remove errorlabstrm in favor of user_err

As noted by @ppedrot, the first is redundant. The patch is basically a renaming.

We didn't make the component optional yet, but this could happen in a
future patch.
---
 tactics/autorewrite.ml |  2 +-
 tactics/eauto.ml       |  6 +++---
 tactics/equality.ml    | 10 +++++-----
 tactics/hints.ml       |  6 +++---
 tactics/hipattern.ml   |  2 +-
 tactics/inv.ml         |  4 ++--
 tactics/leminv.ml      | 10 +++++-----
 tactics/tacticals.ml   |  2 +-
 tactics/tactics.ml     | 50 +++++++++++++++++++++++++-------------------------
 9 files changed, 46 insertions(+), 46 deletions(-)

(limited to 'tactics')

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 3257d406a1..b898ceb046 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -65,7 +65,7 @@ let raw_find_base bas = String.Map.find bas !rewtab
 let find_base bas =
   try raw_find_base bas
   with Not_found ->
-    errorlabstrm "AutoRewrite"
+    user_err "AutoRewrite"
       (str "Rewriting base " ++ str bas ++ str " does not exist.")
 
 let find_rewrites bas =
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 2eca1e597c..dcf3dea106 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -98,7 +98,7 @@ let prolog_tac l n =
   let l = List.map map l in
   try (prolog l n gl)
   with UserError ("Refiner.tclFIRST",_) ->
-    errorlabstrm "Prolog.prolog" (str "Prolog failed.")
+    user_err "Prolog.prolog" (str "Prolog failed.")
   end
 
 open Auto
@@ -431,7 +431,7 @@ let cons a l = a :: l
 let autounfolds db occs cls gl =
   let unfolds = List.concat (List.map (fun dbname -> 
     let db = try searchtable_map dbname 
-      with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
+      with Not_found -> user_err "autounfold" (str "Unknown database " ++ str dbname)
     in
     let (ids, csts) = Hint_db.unfolds db in
     let hyps = pf_ids_of_hyps gl in
@@ -498,7 +498,7 @@ let autounfold_one db cl =
   let st =
     List.fold_left (fun (i,c) dbname -> 
       let db = try searchtable_map dbname 
-	with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
+	with Not_found -> user_err "autounfold" (str "Unknown database " ++ str dbname)
       in
       let (ids, csts) = Hint_db.unfolds db in
 	(Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2c97cf4425..4391a96b17 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -359,7 +359,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 	      let _ = Global.lookup_constant c1' in
 		c1'
 	    with Not_found -> 
-	      errorlabstrm "Equality.find_elim"
+	      user_err "Equality.find_elim"
                 (str "Cannot find rewrite principle " ++ pr_label l' ++ str ".")
 	  end
 	| _ -> destConstRef pr1
@@ -888,7 +888,7 @@ let build_selector env sigma dirn c ind special default =
           on (c bool true) = (c bool false)
           CP : changed assert false in a more informative error
        *)
-      errorlabstrm "Equality.construct_discriminator"
+      user_err "Equality.construct_discriminator"
 	(str "Cannot discriminate on inductive constructors with \
 		 dependent types.") in
   let (indp,_) = dest_ind_family indf in
@@ -974,7 +974,7 @@ let apply_on_clause (f,t) clause =
   let argmv =
     (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
      | Meta mv -> mv
-     | _  -> errorlabstrm "" (str "Ill-formed clause applicator.")) in
+     | _  -> user_err "" (str "Ill-formed clause applicator.")) in
   clenv_fchain ~with_univs:false argmv f_clause clause
 
 let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
@@ -1052,7 +1052,7 @@ let discrEverywhere with_evars =
      else (* <= 8.2 compat *)
        tryAllHypsAndConcl (discrSimpleClause with_evars))
 (*    (fun gls ->
-       errorlabstrm "DiscrEverywhere" (str"No discriminable equalities."))
+       user_err "DiscrEverywhere" (str"No discriminable equalities."))
 *)
 let discr_tac with_evars = function
   | None -> discrEverywhere with_evars
@@ -1725,7 +1725,7 @@ let subst_one_var dep_proof_ok x =
           let hyps = Proofview.Goal.hyps gl in
           let test hyp _ = is_eq_x gl x hyp in
           Context.Named.fold_outside test ~init:() hyps;
-          errorlabstrm "Subst"
+          user_err "Subst"
             (str "Cannot find any non-recursive equality over " ++ pr_id x ++
 	       str".")
         with FoundHyp res -> res in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 8f3eb5eb51..e706316d7b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -632,7 +632,7 @@ let current_pure_db () =
   List.map snd (Hintdbmap.bindings (Hintdbmap.remove "v62" !searchtable))
 
 let error_no_such_hint_database x =
-  errorlabstrm "Hints" (str "No such Hint database: " ++ str x ++ str ".")
+  user_err "Hints" (str "No such Hint database: " ++ str x ++ str ".")
 
 (**************************************************************************)
 (*                       Definition of the summary                        *)
@@ -774,7 +774,7 @@ let make_resolves env sigma flags pri poly ?name cr =
     [make_exact_entry env sigma pri poly ?name; make_apply_entry env sigma flags pri poly ?name]
   in
   if List.is_empty ents then
-    errorlabstrm "Hint"
+    user_err "Hint"
       (pr_lconstr c ++ spc() ++
         (if pi1 flags then str"cannot be used as a hint."
 	else str "can be used as a hint only for eauto."));
@@ -817,7 +817,7 @@ let make_mode ref m =
   let n = List.length ctx in
   let m' = Array.of_list m in
     if not (n == Array.length m') then
-      errorlabstrm "Hint"
+      user_err "Hint"
 	(pr_global ref ++ str" has " ++ int n ++ 
 	   str" arguments while the mode declares " ++ int (Array.length m'))
     else m'
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 6e24cc4698..aee3bc45d5 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -450,7 +450,7 @@ let find_this_eq_data_decompose gl eqn =
     try (*first_match (match_eq eqn) inversible_equalities*)
       find_eq_data eqn
     with PatternMatchingFailure ->
-      errorlabstrm "" (str "No primitive equality found.") in
+      user_err "" (str "No primitive equality found.") in
   let eq_args =
     try extract_eq_args gl eq_args
     with PatternMatchingFailure ->
diff --git a/tactics/inv.ml b/tactics/inv.ml
index bda16b01c0..a7f5ded5bc 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -76,7 +76,7 @@ let make_inv_predicate env evd indf realargs id status concl =
 	    (hyps_arity,concl)
       | Dep dflt_concl ->
 	  if not (occur_var env id concl) then
-	    errorlabstrm "make_inv_predicate"
+	    user_err "make_inv_predicate"
               (str "Current goal does not depend on " ++ pr_id id ++ str".");
           (* We abstract the conclusion of goal with respect to
              realargs and c to * be concl in order to rewrite and have
@@ -440,7 +440,7 @@ let raw_inversion inv_kind id status names =
       try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c)
       with UserError _ ->
         let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in
-        CErrors.errorlabstrm "" msg
+        CErrors.user_err "" msg
     in
     let IndType (indf,realargs) = find_rectype env sigma t in
     let evdref = ref sigma in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 642bf520b1..e83093b0ce 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -183,7 +183,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let ind =
     try find_rectype env sigma i
     with Not_found ->
-      errorlabstrm "inversion_scheme" (no_inductive_inconstr env sigma i)
+      user_err "inversion_scheme" (no_inductive_inconstr env sigma i)
   in
   let (invEnv,invGoal) =
     compute_first_inversion_scheme env sigma ind sort dep_option
@@ -193,7 +193,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
        (global_vars env invGoal)
        (ids_of_named_context (named_context invEnv)));
   (*
-    errorlabstrm "lemma_inversion"
+    user_err "lemma_inversion"
     (str"Computed inversion goal was not closed in initial signature.");
   *)
   let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
@@ -248,7 +248,7 @@ let add_inversion_lemma_exn na com comsort bool tac =
     add_inversion_lemma na env sigma c sort bool tac
   with
     |   UserError ("Case analysis",s) -> (* Reference to Indrec *)
-	  errorlabstrm "Inv needs Nodep Prop Set" s
+	  user_err "Inv needs Nodep Prop Set" s
 
 (* ================================= *)
 (* Applying a given inversion lemma  *)
@@ -261,10 +261,10 @@ let lemInv id c gls =
     Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls
   with
     | NoSuchBinding ->
-	errorlabstrm ""
+	user_err ""
 	  (hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma."))
     | UserError (a,b) ->
-	 errorlabstrm "LemInv"
+	 user_err "LemInv"
 	   (str "Cannot refine current goal with the lemma " ++
 	      pr_lconstr_env (Refiner.pf_env gls) (Refiner.project gls) c)
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 28a7b634c6..c9af1f11ca 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -643,7 +643,7 @@ module New = struct
 	    | Var id -> string_of_id id
 	    | _ -> "\b"
 	  in
-	  errorlabstrm "Tacticals.general_elim_then_using"
+	  user_err "Tacticals.general_elim_then_using"
             (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
     in
     let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ef66e61461..16643b6a75 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -183,7 +183,7 @@ let introduction ?(check=true) id =
     let store = Proofview.Goal.extra gl in
     let env = Proofview.Goal.env gl in
     let () = if check && mem_named_context id hyps then
-      errorlabstrm "Tactics.introduction"
+      user_err "Tactics.introduction"
         (str "Variable " ++ pr_id id ++ str " is already declared.")
     in
     match kind_of_term (whd_evar sigma concl) with
@@ -255,7 +255,7 @@ let clear_dependency_msg env sigma id = function
       Printer.pr_existential env sigma ev ++ str"."
 
 let error_clear_dependency env sigma id err =
-  errorlabstrm "" (clear_dependency_msg env sigma id err)
+  user_err "" (clear_dependency_msg env sigma id err)
 
 let replacing_dependency_msg env sigma id = function
   | Evarutil.OccurHypInSimpleClause None ->
@@ -269,7 +269,7 @@ let replacing_dependency_msg env sigma id = function
       Printer.pr_existential env sigma ev ++ str"."
 
 let error_replacing_dependency env sigma id err =
-  errorlabstrm "" (replacing_dependency_msg env sigma id err)
+  user_err "" (replacing_dependency_msg env sigma id err)
 
 (* This tactic enables the user to remove hypotheses from the signature.
  * Some care is taken to prevent him from removing variables that are
@@ -350,7 +350,7 @@ let rename_hyp repl =
       let () =
         try
           let elt = Id.Set.choose (Id.Set.inter dst mods) in
-          CErrors.errorlabstrm "" (pr_id elt ++ str " is already used")
+          CErrors.user_err "" (pr_id elt ++ str " is already used")
         with Not_found -> ()
       in
       (** All is well *)
@@ -508,7 +508,7 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl ->
     if not (eq_mind sp sp') then
       error "Fixpoints should be on the same mutual inductive declaration.";
     if mem_named_context f (named_context_of_val sign) then
-      errorlabstrm "Logic.prim_refiner"
+      user_err "Logic.prim_refiner"
         (str "Name " ++ pr_id f ++ str " already used in the environment");
     mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
   in
@@ -599,7 +599,7 @@ let pf_reduce_decl redfun where decl gl =
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str " has no value.");
+	user_err "" (pr_id id ++ str " has no value.");
       LocalAssum (id,redfun' ty)
   | LocalDef (id,b,ty) ->
       let b' = if where != InHypTypeOnly then redfun' b else b in
@@ -700,7 +700,7 @@ let pf_e_reduce_decl redfun where decl gl =
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str " has no value.");
+	user_err "" (pr_id id ++ str " has no value.");
     let Sigma (ty', sigma, p) = redfun sigma ty in
     Sigma (LocalAssum (id, ty'), sigma, p)
   | LocalDef (id,b,ty) ->
@@ -740,7 +740,7 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str " has no value.");
+	user_err "" (pr_id id ++ str " has no value.");
     let Sigma (ty', sigma, p) = (redfun false).e_redfun env sigma ty in
     Sigma (LocalAssum (id, ty'), sigma, p)
   | LocalDef (id,b,ty) ->
@@ -778,12 +778,12 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
         isSort (whd_all env sigma t2)
       then (mayneedglobalcheck := true; sigma)
       else
-        errorlabstrm "convert-check-hyp" (str "Types are incompatible.")
+        user_err "convert-check-hyp" (str "Types are incompatible.")
     else sigma
   end
   else
     if not (isSort (whd_all env sigma t1)) then
-      errorlabstrm "convert-check-hyp" (str "Not a type.")
+      user_err "convert-check-hyp" (str "Not a type.")
     else sigma
 
 (* Now we introduce different instances of the previous tacticals *)
@@ -792,7 +792,7 @@ let change_and_check cv_pb mayneedglobalcheck deep t = { e_redfun = begin fun en
   let sigma = Sigma.to_evar_map sigma in
   let sigma = check_types env sigma mayneedglobalcheck deep t' c in
   let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
-  if not b then errorlabstrm "convert-check-hyp" (str "Not convertible.");
+  if not b then user_err "convert-check-hyp" (str "Not convertible.");
   Sigma.Unsafe.of_pair (t', sigma)
 end }
 
@@ -883,7 +883,7 @@ let reduce redexp cl =
 let unfold_constr = function
   | ConstRef sp -> unfold_in_concl [AllOccurrences,EvalConstRef sp]
   | VarRef id -> unfold_in_concl [AllOccurrences,EvalVarRef id]
-  | _ -> errorlabstrm "unfold_constr" (str "Cannot unfold a non-constant.")
+  | _ -> user_err "unfold_constr" (str "Cannot unfold a non-constant.")
 
 (*******************************************)
 (*         Introduction tactics            *)
@@ -1078,7 +1078,7 @@ let depth_of_quantified_hypothesis red h gl =
   match lookup_hypothesis_as_renamed_gen red h gl with
     | Some depth -> depth
     | None ->
-        errorlabstrm "lookup_quantified_hypothesis"
+        user_err "lookup_quantified_hypothesis"
           (str "No " ++ msg_quantified_hypothesis h ++
 	  strbrk " in current goal" ++
 	  (if red then strbrk " even after head-reduction" else mt ()) ++
@@ -1227,7 +1227,7 @@ let cut c =
 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 (Pp.str "unnamed dependent meta")
-  in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
+  in user_err "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
 
 let check_unresolved_evars_of_metas sigma clenv =
   (* This checks that Metas turned into Evars by *)
@@ -1360,7 +1360,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags
   let indmv =
     (match kind_of_term (nth_arg i elimclause.templval.rebus) with
        | Meta mv -> mv
-       | _  -> errorlabstrm "elimination_clause"
+       | _  -> user_err "elimination_clause"
              (str "The type of elimination clause is not well-formed."))
   in
   let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
@@ -1525,7 +1525,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
     try match List.remove Int.equal indmv (clenv_independent elimclause) with
       | [a] -> a
       | _ -> failwith ""
-    with Failure _ -> errorlabstrm "elimination_clause"
+    with Failure _ -> user_err "elimination_clause"
           (str "The type of elimination clause is not well-formed.") in
   let elimclause'  = clenv_fchain ~flags indmv elimclause indclause in
   let hyp = mkVar id in
@@ -1534,7 +1534,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
   let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
   let new_hyp_typ  = clenv_type elimclause'' in
   if Term.eq_constr hyp_typ new_hyp_typ then
-    errorlabstrm "general_rewrite_in"
+    user_err "general_rewrite_in"
       (str "Nothing to rewrite in " ++ pr_id id ++ str".");
   clenv_refine_in with_evars id id sigma elimclause''
     (fun id -> Proofview.tclUNIT ())
@@ -2015,7 +2015,7 @@ let clear_body ids =
     let map = function
     | LocalAssum (id,t) as decl ->
       let () = if List.mem_f Id.equal id ids then
-        errorlabstrm "" (str "Hypothesis " ++ pr_id id ++ str " is not a local definition")
+        user_err "" (str "Hypothesis " ++ pr_id id ++ str " is not a local definition")
       in
       decl
     | LocalDef (id,_,t) as decl ->
@@ -2146,7 +2146,7 @@ let check_number_of_constructors expctdnumopt i nconstr =
   if Int.equal i 0 then error "The constructors are numbered starting from 1.";
   begin match expctdnumopt with
     | Some n when not (Int.equal n nconstr) ->
-	errorlabstrm "Tactics.check_number_of_constructors"
+	user_err "Tactics.check_number_of_constructors"
           (str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ".")
     | _ -> ()
   end;
@@ -2725,7 +2725,7 @@ let enough_by na t tac = forward false (Some (Some tac)) (ipat_of_name na) t
 let generalized_name c t ids cl = function
   | Name id as na ->
       if Id.List.mem id ids then
-	errorlabstrm "" (pr_id id ++ str " is already used.");
+	user_err "" (pr_id id ++ str " is already used.");
       na
   | Anonymous ->
       match kind_of_term c with
@@ -2886,7 +2886,7 @@ let specialize (c,lbind) ipat =
       let tstack = chk tstack in
       let term = applist(thd,List.map (nf_evar clause.evd) tstack) in
       if occur_meta term then
-	errorlabstrm "" (str "Cannot infer an instance for " ++
+	user_err "" (str "Cannot infer an instance for " ++
 
           pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++
 	  str ".");
@@ -2931,7 +2931,7 @@ let unfold_body x =
   (** We normalize the given hypothesis immediately. *)
   let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
   let xval = match Context.Named.lookup x hyps with
-  | LocalAssum _ -> errorlabstrm "unfold_body"
+  | LocalAssum _ -> user_err "unfold_body"
     (pr_id x ++ str" is not a defined hypothesis.")
   | LocalDef (_,xval,_) -> xval
   in
@@ -3428,7 +3428,7 @@ let make_up_names n ind_opt cname =
 
 let error_ind_scheme s =
   let s = if not (String.is_empty s) then s^" " else s in
-  errorlabstrm "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
+  user_err "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
 
 let glob = Universes.constr_of_global
 
@@ -4046,7 +4046,7 @@ let recolle_clenv i params args elimclause gl =
       (fun x ->
 	match kind_of_term x with
 	  | Meta mv -> mv
-	  | _  -> errorlabstrm "elimination_clause"
+	  | _  -> user_err "elimination_clause"
               (str "The type of the elimination clause is not well-formed."))
       arr in
   let k = match i with -1 -> Array.length lindmv - List.length args | _ -> i in
@@ -4193,7 +4193,7 @@ let clear_unselected_context id inhyps cls =
   let open Context.Named.Declaration in
   if occur_var (Tacmach.New.pf_env gl) id (Tacmach.New.pf_concl gl) &&
     cls.concl_occs == NoOccurrences
-  then errorlabstrm ""
+  then user_err ""
     (str "Conclusion must be mentioned: it depends on " ++ pr_id id
      ++ str ".");
   match cls.onhyps with
-- 
cgit v1.2.3