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.

5 files changed, 7 insertions, 7 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f4907e92a..82039abd3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -366,7 +366,7 @@ let check_hidden_implicit_parameters id impls =
     | (Inductive indparams,_,_,_) -> Id.List.mem id indparams
     | _ -> false) impls
   then
-    errorlabstrm "" (strbrk "A parameter of an inductive type " ++
+    user_err "" (strbrk "A parameter of an inductive type " ++
     pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
 
 let push_name_env ?(global_level=false) ntnvars implargs env =
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 588637b76..19f76b972 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -86,7 +86,7 @@ let check_required_library d =
      (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m)
 *)
 (* or failing ...*)
-      errorlabstrm "Coqlib.check_required_library"
+      user_err "Coqlib.check_required_library"
         (str "Library " ++ pr_dirpath dir ++ str " has to be required first.")
 
 (************************************************************************)
diff --git a/interp/notation.ml b/interp/notation.ml
index 0c15e91b8..d50045546 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -95,7 +95,7 @@ let declare_scope scope =
     scope_map := String.Map.add scope empty_scope !scope_map
 
 let error_unknown_scope sc =
-  errorlabstrm "Notation"
+  user_err "Notation"
     (str "Scope " ++ str sc ++ str " is not declared.")
 
 let find_scope scope =
@@ -208,7 +208,7 @@ let remove_delimiters scope =
   let sc = find_scope scope in
   let newsc = { sc with delimiters = None } in
   match sc.delimiters with
-    | None -> CErrors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".")
+    | None -> CErrors.user_err "" (str "No bound key for scope " ++ str scope ++ str ".")
     | Some key ->
        scope_map := String.Map.add scope newsc !scope_map;
        try
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7ab6ebb26..d565f01ba 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -377,7 +377,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) =
   let vars = Id.Map.filter filter nenv.ninterp_var_type in
   let check_recvar x =
     if Id.List.mem x found then
-      errorlabstrm "" (pr_id x ++
+      user_err "" (pr_id x ++
 	strbrk " should only be used in the recursive part of a pattern.") in
   let check (x, y) = check_recvar x; check_recvar y in
   let () = List.iter check foundrec in
@@ -396,7 +396,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) =
   in
   let check_pair s x y where =
     if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then
-      errorlabstrm "" (strbrk "in the right-hand side, " ++ pr_id x ++
+      user_err "" (strbrk "in the right-hand side, " ++ pr_id x ++
 	str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++
 	str " position as part of a recursive pattern.") in
   let check_type x typ =
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index f96d8acc1..1e0964dd2 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -30,7 +30,7 @@ let add_syntax_constant kn c onlyparse =
 
 let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
   if Nametab.exists_cci sp then
-    errorlabstrm "cache_syntax_constant"
+    user_err "cache_syntax_constant"
       (pr_id (basename sp) ++ str " already exists");
   add_syntax_constant kn pat onlyparse;
   Nametab.push_syndef (Nametab.Until i) sp kn