[cleanup] Unify all calls to the error function.

This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.

The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.

We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.

7 files changed, 26 insertions, 26 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 3a263b1e1..08c33b5c1 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -345,7 +345,7 @@ let get_applications mexpr =
   let rec get params = function
     | MEident mp -> mp, params
     | MEapply (fexpr, mp) -> get (mp::params) fexpr
-    | MEwith _ -> error "Non-atomic functor application."
+    | MEwith _ -> user_err Pp.(str "Non-atomic functor application.")
   in get [] mexpr
 
 (** Create the substitution corresponding to some functor applications *)
@@ -353,7 +353,7 @@ let get_applications mexpr =
 let rec compute_subst env mbids sign mp_l inl =
   match mbids,mp_l with
     | _,[] -> mbids,empty_subst
-    | [],r -> error "Application of a functor with too few arguments."
+    | [],r -> user_err Pp.(str "Application of a functor with too few arguments.")
     | mbid::mbids,mp::mp_l ->
 	let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
 	let mb = Environ.lookup_module mp env in
@@ -777,7 +777,7 @@ let rec decompose_functor mpl typ =
   match mpl, typ with
   | [], _ -> typ
   | _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str
-  | _ -> error "Application of a functor with too much arguments."
+  | _ -> user_err Pp.(str "Application of a functor with too much arguments.")
 
 exception NoIncludeSelf
 
diff --git a/library/goptions.ml b/library/goptions.ml
index 9b4fc9985..a803771cb 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -71,7 +71,7 @@ module MakeTable =
 
     let _ =
       if String.List.mem_assoc nick !A.table then
-	error "Sorry, this table name is already used."
+	user_err Pp.(str "Sorry, this table name is already used.")
 
     module MySet = Set.Make (struct type t = A.t let compare = A.compare end)
 
@@ -214,11 +214,11 @@ let get_option key = OptionMap.find key !value_tab
 
 let check_key key = try
   let _ = get_option key in
-  error "Sorry, this option name is already used."
+  user_err Pp.(str "Sorry, this option name is already used.")
 with Not_found ->
   if String.List.mem_assoc (nickname key) !string_table
     || String.List.mem_assoc (nickname key) !ref_table
-  then error "Sorry, this option name is already used."
+  then user_err Pp.(str "Sorry, this option name is already used.")
 
 open Libobject
 
@@ -307,7 +307,7 @@ let set_option_value locality check_and_cast key v =
   | Some (name, depr, (read,write,append)) ->
     write (get_locality locality) (check_and_cast v (read ()))
 
-let bad_type_error () = error "Bad type of value for this option."
+let bad_type_error () = user_err Pp.(str "Bad type of value for this option.")
 
 let check_int_value v = function
   | IntValue _ -> IntValue v
diff --git a/library/impargs.ml b/library/impargs.ml
index a63264b66..885185da1 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -364,7 +364,7 @@ let set_manual_implicits env flags enriching autoimps l =
     with Not_found -> l, None
   in
   if not (List.distinct l) then
-    error ("Some parameters are referred more than once.");
+    user_err Pp.(str "Some parameters are referred more than once.");
   (* Compare with automatic implicits to recover printing data and names *)
   let rec merge k l = function
   | (Name id,imp)::imps ->
@@ -658,7 +658,7 @@ let check_inclusion l =
   let rec aux = function
     | n1::(n2::_ as nl) ->
 	if n1 <= n2 then
-	  error "Sequences of implicit arguments must be of different lengths.";
+	  user_err Pp.(str "Sequences of implicit arguments must be of different lengths.");
 	aux nl
     | _ -> () in
   aux (List.map (fun (imps,_) -> List.length imps) l)
diff --git a/library/lib.ml b/library/lib.ml
index ddd2ed6af..4ad4e261d 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -76,7 +76,7 @@ let classify_segment seg =
     (* LEM; TODO: Understand what this does and see if what I do is the
                   correct thing for ClosedMod(ule|type) *)
     | (_,ClosedModule _) :: stk -> clean acc stk
-    | (_,OpenedSection _) :: _ -> error "there are still opened sections"
+    | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections")
     | (_,OpenedModule (ty,_,_,_)) :: _ ->
       user_err ~hdr:"Lib.classify_segment"
         (str "there are still opened " ++ str (module_kind ty) ++ str "s")
@@ -184,7 +184,7 @@ let split_lib_gen test =
     | [] -> None
   in
     match findeq [] !lib_state.lib_stk with
-      | None -> error "no such entry"
+      | None -> user_err Pp.(str "no such entry")
       | Some r -> r
 
 let eq_object_name (fp1, kn1) (fp2, kn2) =
@@ -222,7 +222,7 @@ let add_anonymous_entry node =
 
 let add_leaf id obj =
   if Names.ModPath.equal (current_mp ()) Names.initial_path then
-    error ("No session module started (use -top dir)");
+    user_err Pp.(str "No session module started (use -top dir)");
   let oname = make_oname id in
   cache_object (oname,obj);
   add_entry oname (Leaf obj);
@@ -272,8 +272,8 @@ let current_mod_id () =
   try match find_entry_p is_opening_node_or_lib with
     | oname,OpenedModule (_,_,_,fs) -> basename (fst oname)
     | oname,CompilingLibrary _ -> basename (fst oname)
-    | _ -> error "you are not in a module"
-  with Not_found -> error "no opened modules"
+    | _ -> user_err Pp.(str "you are not in a module")
+  with Not_found -> user_err Pp.(str "no opened modules")
 
 
 let start_mod is_type export id mp fs =
@@ -305,7 +305,7 @@ let end_mod is_type =
 	else error_still_opened (module_kind ty) oname
       | oname,OpenedSection _ -> error_still_opened "section" oname
       | _ -> assert false
-    with Not_found -> error "No opened modules."
+    with Not_found -> user_err (Pp.str "No opened modules.")
   in
   let (after,mark,before) = split_lib_at_opening oname in
   lib_state := { !lib_state with lib_stk = before };
@@ -326,9 +326,9 @@ let contents_after sp = let (after,_,_) = split_lib sp in after
 (* TODO: use check_for_module ? *)
 let start_compilation s mp =
   if !lib_state.comp_name != None then
-    error "compilation unit is already started";
+    user_err Pp.(str "compilation unit is already started");
   if not (Names.DirPath.is_empty (current_sections ())) then
-    error "some sections are already opened";
+    user_err Pp.(str "some sections are already opened");
   let prefix = s, (mp, Names.DirPath.empty) in
   let () = add_anonymous_entry (CompilingLibrary prefix) in
   lib_state := { !lib_state with comp_name = Some s;
@@ -337,7 +337,7 @@ let start_compilation s mp =
 let end_compilation_checks dir =
   let _ =
     try match snd (find_entry_p is_opening_node) with
-      | OpenedSection _ -> error "There are some open sections."
+      | OpenedSection _ -> user_err Pp.(str  "There are some open sections.")
       | OpenedModule (ty,_,_,_) ->
 	user_err ~hdr:"Lib.end_compilation_checks"
           (str "There are some open " ++ str (module_kind ty) ++ str "s.")
@@ -394,7 +394,7 @@ let find_opening_node id =
       user_err ~hdr:"Lib.find_opening_node"
         (str "Last block to end has name " ++ pr_id id' ++ str ".");
     entry
-  with Not_found -> error "There is nothing to end."
+  with Not_found -> user_err Pp.(str "There is nothing to end.")
 
 (* Discharge tables *)
 
@@ -428,7 +428,7 @@ let add_section () =
 let check_same_poly p vars =
   let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in
   if List.exists pred vars then
-    error "Cannot mix universe polymorphic and monomorphic declarations in sections."
+    user_err Pp.(str  "Cannot mix universe polymorphic and monomorphic declarations in sections.")
 
 let add_section_variable id impl poly ctx =
   match !sectab with
@@ -555,7 +555,7 @@ let close_section () =
       | oname,OpenedSection (_,fs) -> oname,fs
       | _ -> assert false
     with Not_found ->
-      error "No opened section."
+      user_err Pp.(str  "No opened section.")
   in
   let (secdecls,mark,before) = split_lib_at_opening oname in
   lib_state := { !lib_state with lib_stk = before };
diff --git a/library/libnames.ml b/library/libnames.ml
index dd74e192f..50f28b020 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -58,14 +58,14 @@ let add_dirpath_suffix p id = DirPath.make (id :: DirPath.repr p)
 let parse_dir s =
   let len = String.length s in
   let rec decoupe_dirs dirs n =
-    if Int.equal n len && n > 0 then error (s ^ " is an invalid path.");
+    if Int.equal n len && n > 0 then user_err Pp.(str @@ s ^ " is an invalid path.");
     if n >= len then dirs else
     let pos =
       try
 	String.index_from s n '.'
       with Not_found -> len
     in
-    if Int.equal pos n then error (s ^ " is an invalid path.");
+    if Int.equal pos n then user_err Pp.(str @@ s ^ " is an invalid path.");
     let dir = String.sub s n (pos-n) in
     decoupe_dirs ((Id.of_string dir)::dirs) (pos+1)
   in
diff --git a/library/library.ml b/library/library.ml
index 2b3381fa7..5a5f99cc5 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -764,7 +764,7 @@ let save_library_to ?todo dir f otab =
     if !Flags.native_compiler then
       let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
       if not (Nativelib.compile_library dir ast fn) then
-	error "Could not compile the library to native code."
+	user_err Pp.(str "Could not compile the library to native code.")
    with reraise ->
     let reraise = CErrors.push reraise in
     let () = Feedback.msg_warning (str "Removed file " ++ str f') in
diff --git a/library/nametab.ml b/library/nametab.ml
index 1027e291c..2e4e98013 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -143,8 +143,8 @@ struct
 		(* This is an absolute name, we must keep it otherwise it may
 		   become unaccessible forever *)
 		(* But ours is also absolute! This is an error! *)
-		error ("Cannot mask the absolute name \""
-		       ^ U.to_string uname' ^ "\"!")
+		user_err Pp.(str @@ "Cannot mask the absolute name \""
+                                   ^ U.to_string uname' ^ "\"!")
 	  | Nothing
 	  | Relative _ -> mktree (Absolute (uname,o)) tree.map