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.

7 files changed, 18 insertions, 18 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 5e72b8672..f4daa0323 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -609,7 +609,7 @@ let build_scheme fas =
 	      try
 		Smartlocate.global_with_alias f
 	      with Not_found ->
-                errorlabstrm "FunInd.build_scheme"
+                user_err "FunInd.build_scheme"
                   (str "Cannot find " ++ Libnames.pr_reference f)
 	    in
 	    let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
@@ -643,7 +643,7 @@ let build_case_scheme fa =
     let (_,f,_) = fa in
     try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
     with Not_found ->
-      errorlabstrm "FunInd.build_case_scheme"
+      user_err "FunInd.build_case_scheme"
         (str "Cannot find " ++ Libnames.pr_reference f) in
   let first_fun,u = destConst  funs in
   let funs_mp,funs_dp,_ = Names.repr_con first_fun in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 5548833d6..9902b0128 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -630,7 +630,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	let (ind,_) =
 	  try Inductiveops.find_inductive env (Evd.from_env env) b_typ
 	  with Not_found ->
-	    errorlabstrm "" (str "Cannot find the inductive associated to " ++
+	    user_err "" (str "Cannot find the inductive associated to " ++
 			       Printer.pr_glob_constr b ++ str " in " ++
 			       Printer.pr_glob_constr rt ++ str ". try again with a cast")
 	in
@@ -662,7 +662,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	  let (ind,_) =
 	    try Inductiveops.find_inductive env (Evd.from_env env) b_typ
 	    with Not_found ->
-	      errorlabstrm "" (str "Cannot find the inductive associated to " ++
+	      user_err "" (str "Cannot find the inductive associated to " ++
 				 Printer.pr_glob_constr b ++ str " in " ++
 				 Printer.pr_glob_constr rt ++ str ". try again with a cast")
 	  in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 4f183b3a1..943ebc9fc 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -42,7 +42,7 @@ let functional_induction with_clean c princl pat =
 		let finfo = (* we first try to find out a graph on f *)
 		  try find_Function_infos c'
 		  with Not_found ->
-		    errorlabstrm "" (str "Cannot find induction information on "++
+		    user_err "" (str "Cannot find induction information on "++
 				       Printer.pr_lconstr (mkConst c') )
 		in
 		match Tacticals.elimination_sort_of_goal g with
@@ -70,7 +70,7 @@ let functional_induction with_clean c princl pat =
 		    (b,a)
 		    (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *)
 		  with Not_found -> (* This one is neither defined ! *)
-		    errorlabstrm "" (str "Cannot find induction principle for "
+		    user_err "" (str "Cannot find induction principle for "
 				     ++Printer.pr_lconstr (mkConst c') )
 	      in
 	      (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g')
@@ -321,7 +321,7 @@ let error_error names e =
   in
   match e with
     | Building_graph e ->
-	errorlabstrm ""
+	user_err ""
 	  (str "Cannot define graph(s) for " ++
 	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
 	     e_explain e)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index f56e92414..a1c94f8cb 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -110,7 +110,7 @@ let const_of_id id =
   in
   try Constrintern.locate_reference princ_ref
   with Not_found ->
-    CErrors.errorlabstrm "IndFun.const_of_id"
+    CErrors.user_err "IndFun.const_of_id"
       (str "cannot find " ++ Nameops.pr_id id)
 
 let def_of_const t =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 26fc88a60..ee1232013 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1043,19 +1043,19 @@ let invfun qhyp f g =
 			 functional_inversion kn hid  f2 f_correct g
 		       with
 			 | Failure "" ->
-			     errorlabstrm "" (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
+			     user_err "" (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
 			 | Option.IsNone  ->
 			     if do_observe ()
 			     then
 			       error "Cannot use equivalence with graph for any side of the equality"
-			     else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+			     else user_err "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
 			 | Not_found ->
 			     if do_observe ()
 			     then
 			       error "No graph found for any side of equality"
-			     else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+			     else user_err "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
 		   end
-	       | _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ")
+	       | _ -> user_err "" (Ppconstr.pr_id hid ++ str " must be an equality ")
 	  end)
 	  qhyp
           end
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index de4210af5..0b93a909a 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -901,7 +901,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info =
       locate_constant f_ref in
     try find_Function_infos (kn_of_id id)
     with Not_found ->
-      errorlabstrm "indfun" (Nameops.pr_id id ++ str " has no functional scheme")
+      user_err "indfun" (Nameops.pr_id id ++ str " has no functional scheme")
 
 (** [merge id1 id2 args1 args2 id] builds and declares a new inductive
     type called [id], representing the merged graphs of both graphs
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 62f307115..7745e8498 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -307,7 +307,7 @@ let check_not_nested forbidden e =
       | Rel _ -> ()
       | Var x ->
         if Id.List.mem x forbidden
-        then errorlabstrm "Recdef.check_not_nested"
+        then user_err "Recdef.check_not_nested"
                (str "check_not_nested: failure " ++ pr_id x)
       | Meta _ | Evar _ | Sort _ -> ()
       | Cast(e,_,t) -> check_not_nested e;check_not_nested t
@@ -327,7 +327,7 @@ let check_not_nested forbidden e =
   try 
     check_not_nested e 
   with UserError(_,p) -> 
-    errorlabstrm "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p)
+    user_err "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p)
 
 (* ['a info] contains the local information for traveling *)
 type 'a infos = 
@@ -442,7 +442,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	  check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info
 	with e when CErrors.noncritical e ->
-	  errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
+	  user_err "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
       end
     | Lambda(n,t,b) -> 
       begin
@@ -450,7 +450,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	  check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info
 	with e when CErrors.noncritical e ->
-	  errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
+	  user_err "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
       end
     | Case(ci,t,a,l) -> 
       begin
@@ -478,7 +478,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	      jinfo.apP (f,args) expr_info continuation_tac in 
 	    travel_args jinfo
 	      expr_info.is_main_branch new_continuation_tac new_infos
-	  | Case _ ->  errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
+	  | Case _ ->  user_err "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
 	  | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_lconstr expr_info.info)
       end
     | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t}