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.

10 files changed, 20 insertions, 20 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 85c518019e..18ad2ed3d0 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -503,7 +503,7 @@ let set_used_pattern eqn = eqn.used := true
 
 let extract_rhs pb =
   match pb.mat with
-    | [] -> errorlabstrm "build_leaf" (msg_may_need_inversion())
+    | [] -> user_err "build_leaf" (msg_may_need_inversion())
     | eqn::_ ->
 	set_used_pattern eqn;
         eqn.rhs
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 4f265e76c9..92a0ca9887 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -538,7 +538,7 @@ let inheritance_graph () =
 let coercion_of_reference r =
   let ref = Nametab.global r in
   if not (coercion_exists ref) then
-    errorlabstrm "try_add_coercion"
+    user_err "try_add_coercion"
       (Nametab.pr_global_env Id.Set.empty ref ++ str" is not a coercion.");
   ref
 
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 4caa1e9927..c7909a3c7b 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -35,7 +35,7 @@ let explain_occurrence_error = function
   | IncorrectInValueOccurrence id -> explain_incorrect_in_value_occurrence id
 
 let error_occurrences_error e =
-  errorlabstrm "" (explain_occurrence_error e)
+  user_err "" (explain_occurrence_error e)
 
 let error_invalid_occurrence occ =
   error_occurrences_error (InvalidOccurrence occ)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 39aeb41f77..0061d8ae95 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -55,7 +55,7 @@ let is_private mib =
 
 let check_privacy_block mib =
   if is_private mib then
-    errorlabstrm ""(str"case analysis on a private inductive type")
+    user_err ""(str"case analysis on a private inductive type")
       
 (**********************************************************************)
 (* Building case analysis schemes *)
@@ -594,7 +594,7 @@ let lookup_eliminator ind_sp s =
   (* using short name (e.g. for "eq_rec") *)
   try Nametab.locate (qualid_of_ident id)
   with Not_found ->
-    errorlabstrm "default_elim"
+    user_err "default_elim"
       (strbrk "Cannot find the elimination combinator " ++
        pr_id id ++ strbrk ", the elimination of the inductive definition " ++
        pr_global_env Id.Set.empty (IndRef ind_sp) ++
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 214e19fecf..cb69ab36f2 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -355,7 +355,7 @@ let make_case_or_project env indf ci pred c branches =
        let mib, _ = Inductive.lookup_mind_specif env ind in
        if (* dependent *) not (noccurn 1 t) &&
           not (has_dependent_elim mib) then
-       errorlabstrm "make_case_or_project"
+       user_err "make_case_or_project"
 		    Pp.(str"Dependent case analysis not allowed" ++
 		     str" on inductive type " ++ Names.MutInd.print (fst ind))
      in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 99c3772db9..aa795106a8 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -204,7 +204,7 @@ let error_instantiate_pattern id l =
   | [_] -> "is" 
   | _ -> "are"
   in
-  errorlabstrm "" (str "Cannot substitute the term bound to " ++ pr_id id
+  user_err "" (str "Cannot substitute the term bound to " ++ pr_id id
     ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l
     ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8b0bdb0092..cdb39207e5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -390,7 +390,7 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function
       try Name (Id.Map.find id ltac_idents)
       with Not_found ->
         if Id.Map.mem id ltac_genargs then
-          errorlabstrm "" (str"Ltac variable"++spc()++ pr_id id ++
+          user_err "" (str"Ltac variable"++spc()++ pr_id id ++
                            spc()++str"is not bound to an identifier."++spc()++
                            str"It cannot be used in a binder.")
         else n
@@ -411,14 +411,14 @@ let invert_ltac_bound_name lvar env id0 id =
   let id' = Id.Map.find id lvar.ltac_idents in
   try mkRel (pi1 (lookup_rel_id id' (rel_context env)))
   with Not_found ->
-    errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
+    user_err "" (str "Ltac variable " ++ pr_id id0 ++
 		       str " depends on pattern variable name " ++ pr_id id ++
 		       str " which is not bound in current context.")
 
 let protected_get_type_of env sigma c =
   try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c
   with Retyping.RetypeError _ ->
-    errorlabstrm ""
+    user_err ""
       (str "Cannot reinterpret " ++ quote (print_constr c) ++
        str " in the current environment.")
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 284af0cb15..945ef5daac 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -291,7 +291,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
 (*s High-level declaration of a canonical structure *)
 
 let error_not_structure ref =
-  errorlabstrm "object_declare"
+  user_err "object_declare"
     (Nameops.pr_id (basename_of_global ref) ++ str" is not a structure object.")
 
 let check_and_decompose_canonical_structure ref =
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 820a81b5d2..67819dc986 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -38,7 +38,7 @@ exception Elimconst
 exception Redelimination
 
 let error_not_evaluable r =
-  errorlabstrm "error_not_evaluable"
+  user_err "error_not_evaluable"
     (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++
      spc () ++ str "to an evaluable reference.")
 
@@ -993,7 +993,7 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
       incr pos;
       if ok then begin
         if Option.has_some nested then
-          errorlabstrm "" (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str ".");
+          user_err "" (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str ".");
         (* Skip inner occurrences for stable counting of occurrences *)
         if locs != [] then
           ignore (traverse_below (Some (!pos-1)) envc t);
@@ -1159,13 +1159,13 @@ let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
 let check_privacy env ind =
   let spec = Inductive.lookup_mind_specif env (fst ind) in
   if Inductive.is_private spec then
-    errorlabstrm "" (str "case analysis on a private type.")
+    user_err "" (str "case analysis on a private type.")
   else ind
 
 let check_not_primitive_record env ind =
   let spec = Inductive.lookup_mind_specif env (fst ind) in
     if Inductive.is_primitive_record spec then
-      errorlabstrm "" (str "case analysis on a primitive record type: " ++
+      user_err "" (str "case analysis on a primitive record type: " ++
 		       str "use projections or let instead.")
     else ind
 
@@ -1182,14 +1182,14 @@ let reduce_to_ind_gen allow_product env sigma t =
 	  if allow_product then
 	    elimrec (push_rel (LocalAssum (n,ty)) env) t' ((LocalAssum (n,ty))::l)
 	  else
-	    errorlabstrm "" (str"Not an inductive definition.")
+	    user_err "" (str"Not an inductive definition.")
       | _ ->
 	  (* Last chance: we allow to bypass the Opaque flag (as it
 	     was partially the case between V5.10 and V8.1 *)
 	  let t' = whd_all env sigma t in
 	  match kind_of_term (fst (decompose_app t')) with
 	    | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l)
-	    | _ -> errorlabstrm "" (str"Not an inductive product.")
+	    | _ -> user_err "" (str"Not an inductive product.")
   in
   elimrec env t []
 
@@ -1239,7 +1239,7 @@ let one_step_reduce env sigma c =
   applist (redrec (c,[]))
 
 let error_cannot_recognize ref =
-  errorlabstrm ""
+  user_err ""
     (str "Cannot recognize a statement based on " ++
      Nametab.pr_global_env Id.Set.empty ref ++ str".")
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0c1ce0d2f8..5e3c3c2598 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1586,7 +1586,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     let ids = ids_of_named_context (named_context env) in
     if name == Anonymous then next_ident_away_in_goal x ids else
     if mem_named_context x (named_context env) then
-      errorlabstrm "Unification.make_abstraction_core"
+      user_err "Unification.make_abstraction_core"
         (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.")
     else
       x
@@ -1600,7 +1600,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
         if indirectly_dependent c d depdecls then
           (* Told explicitly not to abstract over [d], but it is dependent *)
           let id' = indirect_dependency d depdecls in
-          errorlabstrm "" (str "Cannot abstract over " ++ Nameops.pr_id id'
+          user_err "" (str "Cannot abstract over " ++ Nameops.pr_id id'
             ++ str " without also abstracting or erasing " ++ Nameops.pr_id hyp
             ++ str ".")
         else