[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.

9 files changed, 99 insertions, 99 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 5843da31e..004083dcf 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -353,7 +353,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 		(match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ();
 	       id)
 	end
-      else CErrors.error "Unsolved obligations remaining.")
+      else CErrors.user_err Pp.(str "Unsolved obligations remaining."))
 	
 let named_of_rel_context l =
   let acc, ctx =
@@ -379,7 +379,7 @@ let context poly l =
   let ctx =
     try named_of_rel_context fullctx
     with e when CErrors.noncritical e ->
-      error "Anonymous variables not allowed in contexts."
+      user_err Pp.(str "Anonymous variables not allowed in contexts.")
   in
   let uctx = ref (Evd.universe_context_set !evars) in
   let fn status (id, b, t) =
diff --git a/vernac/command.ml b/vernac/command.ml
index 8a9bbb884..4b29700e5 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -382,7 +382,7 @@ type structured_inductive_expr =
   local_binder_expr list * structured_one_inductive_expr list
 
 let minductive_message warn = function
-  | []  -> error "No inductive definition."
+  | []  -> user_err Pp.(str "No inductive definition.")
   | [x] -> (pr_id x ++ str " is defined" ++ 
 	    if warn then str " as a non-primitive record" else mt())
   | l   -> hov 0  (prlist_with_sep pr_comma pr_id l ++
@@ -676,8 +676,8 @@ let extract_params indl =
   match paramsl with
   | [] -> anomaly (Pp.str "empty list of inductive types")
   | params::paramsl ->
-      if not (List.for_all (eq_local_binders params) paramsl) then error
-	"Parameters should be syntactically the same for each inductive type.";
+      if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str
+	"Parameters should be syntactically the same for each inductive type.");
       params
 
 let extract_inductive indl =
@@ -715,9 +715,9 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
   begin match mie.mind_entry_finite with
   | BiFinite when is_recursive mie ->
       if Option.has_some mie.mind_entry_record then
-        error "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command."
+        user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.")
       else
-        error ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.")
+        user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command."))
   | _ -> ()
   end;
   let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
@@ -1122,7 +1122,7 @@ let interp_recursive isfix fixl notations =
         | x , None -> x
         | Some ls , Some us ->
 	   if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) ls us) then
-	     error "(co)-recursive definitions should all have the same universe binders";
+	     user_err Pp.(str "(co)-recursive definitions should all have the same universe binders");
 	   Some us) fixl None in
   let ctx = Evd.make_evar_universe_context env all_universes in
   let evdref = ref (Evd.from_ctx ctx) in
@@ -1262,8 +1262,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
 let extract_decreasing_argument limit = function
   | (na,CStructRec) -> na
   | (na,_) when not limit -> na
-  | _ -> error 
-      "Only structural decreasing is supported for a non-Program Fixpoint"
+  | _ -> user_err Pp.(str 
+      "Only structural decreasing is supported for a non-Program Fixpoint")
 
 let extract_fixpoint_components limit l =
   let fixl, ntnl = List.split l in
@@ -1282,7 +1282,7 @@ let extract_cofixpoint_components l =
 
 let out_def = function
   | Some def -> def
-  | None -> error "Program Fixpoint needs defined bodies."
+  | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.")
 
 let collect_evars_of_term evd c ty =
   let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in
diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml
index c6588684a..f3259f1f3 100644
--- a/vernac/ind_tables.ml
+++ b/vernac/ind_tables.ml
@@ -81,7 +81,7 @@ let scheme_object_table =
 let declare_scheme_object s aux f =
   let () =
     if not (Id.is_valid ("ind" ^ s)) then
-      error ("Illegal induction scheme suffix: " ^ s)
+      user_err Pp.(str ("Illegal induction scheme suffix: " ^ s))
   in
   let key = if String.is_empty aux then s else aux in
   try
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index b21e80bef..a78221301 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -418,7 +418,7 @@ let get_common_underlying_mutual_inductive = function
 	  raise (RecursionSchemeError (NotMutualInScheme (ind,ind')))
       | [] ->
 	  if not (List.distinct_f Int.compare (List.map snd (List.map snd all)))
-          then error "A type occurs twice";
+          then user_err Pp.(str "A type occurs twice");
 	  mind,
 	  List.map_filter
 	    (function (Some id,(_,i)) -> Some (i,snd id) | (None,_) -> None) all
@@ -429,7 +429,7 @@ let do_scheme l =
 tried to declare different schemes at once *)
     if not (List.is_empty ischeme) && not (List.is_empty escheme)
     then
-      error "Do not declare equality and induction scheme at the same time."
+      user_err Pp.(str "Do not declare equality and induction scheme at the same time.")
     else (
       if not (List.is_empty ischeme) then do_mutual_induction_scheme ischeme
       else
@@ -497,7 +497,7 @@ let do_combined_scheme name schemes =
 		let refe = Ident x in
 		let qualid = qualid_of_reference refe in
 		try Nametab.locate_constant (snd qualid)
-                with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared."))
+                with Not_found -> user_err Pp.(pr_qualid (snd qualid) ++ str " is not declared."))
       schemes
   in
   let body,typ = build_combined_scheme (Global.env ()) csts in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index c67a3302f..d6ae0ea86 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -153,9 +153,9 @@ let find_mutually_recursive_statements thms =
 	  (* assume the largest indices as possible *)
 	  List.last common_same_indhyp, false, possible_guards
       | _, [] ->
-	  error
+	  user_err Pp.(str
             ("Cannot find common (mutual) inductive premises or coinductive" ^
-             " conclusions in the statements.")
+             " conclusions in the statements."))
     in
     (finite,guard,None), ordered_inds
 
@@ -273,7 +273,7 @@ let save_named ?export_seff proof =
 
 let check_anonymity id save_ident =
   if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
-    error "This command can only be used for unnamed theorem."
+    user_err Pp.(str "This command can only be used for unnamed theorem.")
 
 let save_anonymous ?export_seff proof save_ident =
   let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
@@ -478,10 +478,10 @@ let save_proof ?proof = function
         match proof with
         | Some ({ id; entries; persistence = k; universes }, _) ->
             if List.length entries <> 1 then
-              error "Admitted does not support multiple statements";
+              user_err Pp.(str "Admitted does not support multiple statements");
             let { const_entry_secctx; const_entry_type } = List.hd entries in
             if const_entry_type = None then
-              error "Admitted requires an explicit statement";
+              user_err Pp.(str "Admitted requires an explicit statement");
             let typ = Option.get const_entry_type in
             let ctx = Evd.evar_context_universe_context (fst universes) in
             let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
diff --git a/vernac/locality.ml b/vernac/locality.ml
index 03640676e..a25acb0d3 100644
--- a/vernac/locality.ml
+++ b/vernac/locality.ml
@@ -35,9 +35,9 @@ let enforce_locality_full locality_flag local =
   let local =
     match locality_flag with
     | Some false when local ->
-	CErrors.error "Cannot be simultaneously Local and Global."
+	CErrors.user_err Pp.(str "Cannot be simultaneously Local and Global.")
     | Some true when local ->
-	CErrors.error "Use only prefix \"Local\"."
+	CErrors.user_err Pp.(str "Use only prefix \"Local\".")
     | None ->
 	if local then begin
 	    warn_deprecated_local_syntax ();
@@ -66,7 +66,7 @@ let enforce_locality_exp locality_flag local =
   | None, Some local -> local
   | Some b, None -> local_of_bool b
   | None, None -> Decl_kinds.Global
-  | Some _, Some _ -> CErrors.error "Local non allowed in this case"
+  | Some _, Some _ -> CErrors.user_err Pp.(str "Local non allowed in this case")
 
 (* For commands whose default is to not discharge but to export:
    Global in sections forces discharge, Global not in section is the default;
@@ -87,8 +87,8 @@ let enforce_section_locality locality_flag local =
 let make_module_locality = function
   | Some false ->
       if Lib.sections_are_opened () then
-	CErrors.error
-	  "This command does not support the Global option in sections.";
+	CErrors.user_err Pp.(str
+	  "This command does not support the Global option in sections.");
       false
   | Some true -> true
   | None -> false
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index fb7c72941..42494dd28 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -60,7 +60,7 @@ let pr_entry e =
 let pr_registered_grammar name =
   let gram = try Some (String.Map.find name !grammars) with Not_found -> None in
   match gram with
-  | None -> error "Unknown or unprintable grammar entry."
+  | None -> user_err Pp.(str "Unknown or unprintable grammar entry.")
   | Some entries ->
     let pr_one (AnyEntry e) =
       str "Entry " ++ str (Pcoq.Gram.Entry.name e) ++ str " is" ++ fnl () ++
@@ -107,11 +107,11 @@ let parse_format ((loc, str) : lstring) =
     if Int.equal n 0 then l else push_token (UnpTerminal (String.make n ' ')) l in
   let close_box i b = function
     | a::(_::_ as l) -> push_token (UnpBox (b,a)) l
-    | _ -> error "Non terminated box in format." in
+    | _ -> user_err Pp.(str "Non terminated box in format.") in
   let close_quotation i =
     if i < String.length str && str.[i] == '\'' && (Int.equal (i+1) l || str.[i+1] == ' ')
     then i+1
-    else error "Incorrectly terminated quoted expression." in
+    else user_err Pp.(str "Incorrectly terminated quoted expression.") in
   let rec spaces n i =
     if i < String.length str && str.[i] == ' ' then spaces (n+1) (i+1)
     else n in
@@ -119,10 +119,10 @@ let parse_format ((loc, str) : lstring) =
     if i < String.length str && str.[i] != ' ' then
       if str.[i] == '\'' && quoted &&
         (i+1 >= String.length str || str.[i+1] == ' ')
-      then if Int.equal n 0 then error "Empty quoted token." else n
+      then if Int.equal n 0 then user_err Pp.(str "Empty quoted token.") else n
       else nonspaces quoted (n+1) (i+1)
     else
-      if quoted then error "Spaces are not allowed in (quoted) symbols."
+      if quoted then user_err Pp.(str "Spaces are not allowed in (quoted) symbols.")
       else n in
   let rec parse_non_format i =
     let n = nonspaces false 0 i in
@@ -153,8 +153,8 @@ let parse_format ((loc, str) : lstring) =
 		(* Parse " [ .. ",  *)
 	    | ' ' | '\'' ->
 		parse_box (fun n -> PpHOVB n) (i+1)
-	    | _ -> error "\"v\", \"hv\", \" \" expected after \"[\" in format."
-	  else error "\"v\", \"hv\" or \" \" expected after \"[\" in format."
+	    | _ -> user_err Pp.(str "\"v\", \"hv\", \" \" expected after \"[\" in format.")
+	  else user_err Pp.(str "\"v\", \"hv\" or \" \" expected after \"[\" in format.")
       (* Parse "]"  *)
       | ']' ->
 	  ([] :: parse_token (close_quotation (i+1)))
@@ -165,7 +165,7 @@ let parse_format ((loc, str) : lstring) =
 	    (parse_token (close_quotation (i+n))))
     else
       if Int.equal n 0 then []
-      else error "Ending spaces non part of a format annotation."
+      else user_err Pp.(str "Ending spaces non part of a format annotation.")
   and parse_box box i =
     let n = spaces 0 i in
     close_box i (box n) (parse_token (close_quotation (i+n)))
@@ -187,9 +187,9 @@ let parse_format ((loc, str) : lstring) =
   try
     if not (String.is_empty str) then match parse_token 0 with
       | [l] -> l
-      | _ -> error "Box closed without being opened in format."
+      | _ -> user_err Pp.(str "Box closed without being opened in format.")
     else
-      error "Empty format."
+      user_err Pp.(str "Empty format.")
   with reraise ->
     let (e, info) = CErrors.push reraise in
     let info = Option.cata (Loc.add_loc info) info loc in
@@ -243,19 +243,19 @@ let rec find_pattern nt xl = function
   | [], NonTerminal x' :: l' ->
       (out_nt nt,x',List.rev xl),l'
   | _, Break s :: _ | Break s :: _, _ ->
-      error ("A break occurs on one side of \"..\" but not on the other side.")
+      user_err Pp.(str ("A break occurs on one side of \"..\" but not on the other side."))
   | _, Terminal s :: _ | Terminal s :: _, _ ->
       user_err ~hdr:"Metasyntax.find_pattern"
         (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.")
   | _, [] ->
-      error msg_expected_form_of_recursive_notation
+      user_err Pp.(str msg_expected_form_of_recursive_notation)
   | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->
       anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right")
 
 let rec interp_list_parser hd = function
   | [] -> [], List.rev hd
   | NonTerminal id :: tl when Id.equal id ldots_var ->
-      if List.is_empty hd then error msg_expected_form_of_recursive_notation;
+      if List.is_empty hd then user_err Pp.(str msg_expected_form_of_recursive_notation);
       let hd = List.rev hd in
       let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
       let xyl,tl'' = interp_list_parser [] tl' in
@@ -286,7 +286,7 @@ let quote_notation_token x =
 let rec raw_analyze_notation_tokens = function
   | []    -> []
   | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl
-  | String "_" :: _ -> error "_ must be quoted."
+  | String "_" :: _ -> user_err Pp.(str "_ must be quoted.")
   | String x :: sl when CLexer.is_ident x ->
       NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl
   | String s :: sl ->
@@ -487,7 +487,7 @@ let make_hunks etyps symbols from =
 
 (* Build default printing rules from explicit format *)
 
-let error_format () = error "The format does not match the notation."
+let error_format () = user_err Pp.(str "The format does not match the notation.")
 
 let rec split_format_at_ldots hd = function
   | UnpTerminal s :: fmt when String.equal s (Id.to_string ldots_var) -> List.rev hd, fmt
@@ -500,7 +500,7 @@ and check_no_ldots_in_box = function
   | UnpBox (_,fmt) ->
       (try
         let _ = split_format_at_ldots [] fmt in
-        error ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse.")
+        user_err Pp.(str ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse."))
       with Exit -> ())
   | _ -> ()
 
@@ -518,7 +518,7 @@ let read_recursive_format sl fmt =
   let rec get_tail = function
     | a :: sepfmt, b :: fmt when Pervasives.(=) a b -> get_tail (sepfmt, fmt) (* FIXME *)
     | [], tail -> skip_var_in_recursive_format tail
-    | _ -> error "The format is not the same on the right and left hand side of the special token \"..\"." in
+    | _ -> user_err Pp.(str "The format is not the same on the right and left hand side of the special token \"..\".") in
   let slfmt, fmt = get_head fmt in
   slfmt, get_tail (slfmt, fmt)
 
@@ -652,7 +652,7 @@ let make_production etyps symbols =
 		distribute
                   [GramConstrNonTerminal (ETBinderList (o,tkl), Some x)] ll
             | _ ->
-                error "Components of recursive patterns in notation must be terms or binders.")
+                user_err Pp.(str "Components of recursive patterns in notation must be terms or binders."))
       symbols [[]] in
   List.map define_keywords prod
 
@@ -811,7 +811,7 @@ let interp_modifiers modl = let open NotationMods in
 
         interp { acc with level = Some n; } l
     | SetAssoc a :: l ->
-	if not (Option.is_empty acc.assoc) then error "An associativity is given more than once.";
+	if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once.");
         interp { acc with assoc = Some a; } l
      | SetOnlyParsing :: l ->
         interp { acc with only_parsing = true; } l
@@ -820,7 +820,7 @@ let interp_modifiers modl = let open NotationMods in
     | SetCompatVersion v :: l ->
         interp { acc with compat = Some v; } l
     | SetFormat ("text",s) :: l ->
-	if not (Option.is_empty acc.format) then error "A format is given more than once.";
+	if not (Option.is_empty acc.format) then user_err Pp.(str "A format is given more than once.");
         interp { acc with format = Some s; } l
     | SetFormat (k,(_,s)) :: l ->
         interp { acc with extra = (k,s)::acc.extra; } l
@@ -829,7 +829,7 @@ let interp_modifiers modl = let open NotationMods in
 let check_infix_modifiers modifiers =
   let t = (interp_modifiers modifiers).NotationMods.etyps in
   if not (List.is_empty t) then
-    error "Explicit entry level or type unexpected in infix notation."
+    user_err Pp.(str "Explicit entry level or type unexpected in infix notation.")
 
 let check_useless_entry_types recvars mainvars etyps =
   let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in
@@ -901,7 +901,7 @@ let internalization_type_of_entry_type = function
   | ETBigint | ETReference -> NtnInternTypeConstr
   | ETBinder _ -> NtnInternTypeBinder
   | ETName -> NtnInternTypeIdent
-  | ETPattern | ETOther _ -> error "Not supported."
+  | ETPattern | ETOther _ -> user_err Pp.(str "Not supported.")
   | ETBinderList _ | ETConstrList _ -> assert false
 
 let set_internalization_type typs =
@@ -917,7 +917,7 @@ let make_interpretation_type isrec isonlybinding = function
   | NtnInternTypeConstr | NtnInternTypeIdent ->
      if isonlybinding then NtnTypeOnlyBinder else NtnTypeConstr
   | NtnInternTypeBinder when isrec -> NtnTypeBinderList
-   | NtnInternTypeBinder -> error "Type binder is only for use in recursive notations for binders."
+   | NtnInternTypeBinder -> user_err Pp.(str "Type binder is only for use in recursive notations for binders.")
 
 let make_interpretation_vars recvars allvars =
   let eq_subscope (sc1, l1) (sc2, l2) =
@@ -938,9 +938,9 @@ let make_interpretation_vars recvars allvars =
 
 let check_rule_productivity l =
   if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then
-    error "A notation must include at least one symbol.";
+    user_err Pp.(str "A notation must include at least one symbol.");
   if (match l with SProdList _ :: _ -> true | _ -> false) then
-    error "A recursive notation must start with at least one symbol."
+    user_err Pp.(str "A recursive notation must start with at least one symbol.")
 
 let warn_notation_bound_to_variable =
   CWarnings.create ~name:"notation-bound-to-variable" ~category:"parsing"
@@ -980,7 +980,7 @@ let find_precedence lev etyps symbols =
   | Some (NonTerminal x) ->
       (try match List.assoc x etyps with
 	| ETConstr _ ->
-	    error "The level of the leftmost non-terminal cannot be changed."
+	    user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.")
 	| ETName | ETBigint | ETReference ->
             begin match lev with
             | None ->
@@ -988,31 +988,31 @@ let find_precedence lev etyps symbols =
             | Some 0 ->
               ([],0)
             | _ ->
-	      error "A notation starting with an atomic expression must be at level 0."
+	      user_err Pp.(str "A notation starting with an atomic expression must be at level 0.")
             end
 	| ETPattern | ETBinder _ | ETOther _ -> (* Give a default ? *)
 	    if Option.is_empty lev then
-	      error "Need an explicit level."
+	      user_err Pp.(str "Need an explicit level.")
 	    else [],Option.get lev
         | ETConstrList _ | ETBinderList _ ->
 	    assert false (* internally used in grammar only *)
       with Not_found ->
 	if Option.is_empty lev then
-	  error "A left-recursive notation must have an explicit level."
+	  user_err Pp.(str "A left-recursive notation must have an explicit level.")
 	else [],Option.get lev)
   | Some (Terminal _) when last_is_terminal () ->
       if Option.is_empty lev then
 	([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0)
       else [],Option.get lev
   | Some _ ->
-      if Option.is_empty lev then error "Cannot determine the level.";
+      if Option.is_empty lev then user_err Pp.(str "Cannot determine the level.");
       [],Option.get lev
 
 let check_curly_brackets_notation_exists () =
   try let _ = Notation.level_of_notation "{ _ }" in ()
   with Not_found ->
-    error "Notations involving patterns of the form \"{ _ }\" are treated \n\
-specially and require that the notation \"{ _ }\" is already reserved."
+    user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\
+specially and require that the notation \"{ _ }\" is already reserved.")
 
 (* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *)
 let remove_curly_brackets l =
@@ -1081,7 +1081,7 @@ let compute_syntax_data df modifiers =
   let mods = interp_modifiers modifiers in
   let onlyprint = mods.only_printing in
   let onlyparse = mods.only_parsing in
-  if onlyprint && onlyparse then error "A notation cannot be both 'only printing' and 'only parsing'.";
+  if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
   let assoc = Option.append mods.assoc (Some NonA) in
   let toks = split_notation_string df in
   let recvars,mainvars,symbols = analyze_notation_tokens toks in
@@ -1385,7 +1385,7 @@ let set_notation_for_interpretation impls ((_,df),c,sc) =
   (try ignore
     (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ());
   with NoSyntaxRule ->
-    error "Parsing rule for this notation has to be previously declared.");
+    user_err Pp.(str "Parsing rule for this notation has to be previously declared."));
   Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
 
 (* Main entry point *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 10207d0e0..5accc8e37 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -561,7 +561,7 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id
   in
   let isnot_class = match kind with Class false -> false | _ -> true in
   if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
-    error "Priorities only allowed for type class substructures";
+    user_err Pp.(str "Priorities only allowed for type class substructures");
   (* Now, younger decl in params and fields is on top *)
   let (pl, ctx), arity, template, implpars, params, implfs, fields =
     States.with_state_protection (fun () ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a08c79c40..6c1d64cfe 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -139,7 +139,7 @@ let make_cases s =
 let show_match id =
   let patterns =
     try make_cases_aux (Nametab.global id)
-    with Not_found -> error "Unknown inductive type."
+    with Not_found -> user_err Pp.(str "Unknown inductive type.")
   in
   let pr_branch l =
     str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>"
@@ -305,7 +305,7 @@ let print_strategy r =
     let key = match r with
     | VarRef id -> VarKey id
     | ConstRef cst -> ConstKey cst
-    | IndRef _ | ConstructRef _ -> error "The reference is not unfoldable"
+    | IndRef _ | ConstructRef _ -> user_err Pp.(str "The reference is not unfoldable")
     in
     let lvl = get_strategy oracle key in
     Feedback.msg_notice (pr_strategy (r, lvl))
@@ -451,8 +451,8 @@ let start_proof_and_print k l hook =
                                    concl (Tacticals.New.tclCOMPLETE tac)
           in Evd.set_universe_context sigma ctx, EConstr.of_constr c
         with Logic_monad.TacticFailure e when Logic.catchable_exception e ->
-          error "The statement obligations could not be resolved \
-                 automatically, write a statement definition first."
+          user_err Pp.(str "The statement obligations could not be resolved \
+                 automatically, write a statement definition first.")
       in Some hook
     else None
   in
@@ -551,9 +551,9 @@ let vernac_inductive poly lo finite indl =
       indl;
   match indl with
   | [ ( _ , _ , _ ,(Record|Structure), Constructors _ ),_ ] ->
-      CErrors.error "The Record keyword is for types defined using the syntax { ... }."
+      user_err Pp.(str "The Record keyword is for types defined using the syntax { ... }.")
   | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] ->
-      CErrors.error "The Variant keyword does not support syntax { ... }."
+      user_err Pp.(str "The Variant keyword does not support syntax { ... }.")
   | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
       vernac_record (match b with Class _ -> Class false | _ -> b)
        poly finite id bl c oc fs
@@ -564,16 +564,16 @@ let vernac_inductive poly lo finite indl =
   	  (((coe', AssumExpr ((loc, Name id), ce)), None), [])
       in vernac_record (Class true) poly finite id bl c None [f]
   | [ ( _ , _, _, Class _, Constructors _), [] ] ->
-      CErrors.error "Inductive classes not supported"
+      user_err Pp.(str "Inductive classes not supported")
   | [ ( id , bl , c , Class _, _), _ :: _ ] ->
-      CErrors.error "where clause not supported for classes"
+      user_err Pp.(str "where clause not supported for classes")
   | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] ->
-      CErrors.error "where clause not supported for (co)inductive records"
+      user_err Pp.(str "where clause not supported for (co)inductive records")
   | _ -> let unpack = function
       | ( (false, id) , bl , c , _ , Constructors l ) , ntn  -> ( id , bl , c , l ) , ntn
       | ( (true,_),_,_,_,Constructors _),_ ->
-          CErrors.error "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead."
-      | _ -> CErrors.error "Cannot handle mutually (co)inductive records."
+          user_err Pp.(str "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead.")
+      | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.")
     in
     let indl = List.map unpack indl in
     do_mutual_inductive indl poly lo finite
@@ -631,11 +631,11 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
   (* We check the state of the system (in section, in module type)
      and what module information is supplied *)
   if Lib.sections_are_opened () then
-    error "Modules and Module Types are not allowed inside sections.";
+    user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
   let binders_ast = List.map
    (fun (export,idl,ty) ->
      if not (Option.is_empty export) then
-      error "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument."
+      user_err Pp.(str "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument.")
      else (idl,ty)) binders_ast in
   let mp =
     Declaremods.declare_module Modintern.interp_module_ast
@@ -649,7 +649,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
   (* We check the state of the system (in section, in module type)
      and what module information is supplied *)
   if Lib.sections_are_opened () then
-    error "Modules and Module Types are not allowed inside sections.";
+    user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
   match mexpr_ast_l with
     | [] ->
        check_no_pending_proofs ();
@@ -674,7 +674,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
        let binders_ast = List.map
         (fun (export,idl,ty) ->
           if not (Option.is_empty export) then
-           error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument."
+           user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.")
           else (idl,ty)) binders_ast in
        let mp =
          Declaremods.declare_module Modintern.interp_module_ast
@@ -694,7 +694,7 @@ let vernac_end_module export (loc,id as lid) =
 
 let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
   if Lib.sections_are_opened () then
-    error "Modules and Module Types are not allowed inside sections.";
+    user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
 
   match mty_ast_l with
     | [] ->
@@ -722,7 +722,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
 	let binders_ast = List.map
           (fun (export,idl,ty) ->
             if not (Option.is_empty export) then
-              error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument."
+              user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.")
             else (idl,ty)) binders_ast in
 	let mp =
           Declaremods.declare_modtype Modintern.interp_module_ast
@@ -846,7 +846,7 @@ let vernac_set_end_tac tac =
   let env = Genintern.empty_glob_sign (Global.env ()) in
   let _, tac = Genintern.generic_intern env tac in
   if not (refining ()) then
-    error "Unknown command of the non proof-editing mode.";
+    user_err Pp.(str "Unknown command of the non proof-editing mode.");
   set_end_tac tac
     (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
 
@@ -903,7 +903,7 @@ let vernac_chdir = function
 	  (* Cd is typically used to control the output directory of
 	  extraction. A failed Cd could lead to overwriting .ml files
 	  so we make it an error. *)
-	  CErrors.error ("Cd failed: " ^ err)
+	  user_err Pp.(str ("Cd failed: " ^ err))
       end;
       if_verbose Feedback.msg_info (str (Sys.getcwd()))
 
@@ -972,7 +972,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
   let never_unfold_flag = List.mem `ReductionNeverUnfold flags in
 
   let err_incompat x y =
-    error ("Options \""^x^"\" and \""^y^"\" are incompatible.") in
+    user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in
 
   if assert_flag && rename_flag then
     err_incompat "assert" "rename";
@@ -1018,7 +1018,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
     | { name = Anonymous; notation_scope = Some _ } :: args ->
        check_extra_args args
     | _ ->
-       error "Extra notation scopes can be set on anonymous and explicit arguments only."
+       user_err Pp.(str "Extra notation scopes can be set on anonymous and explicit arguments only.")
   in
 
   let args, scopes =
@@ -1032,12 +1032,12 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
   in
 
   if Option.cata (fun n -> n > num_args) false nargs_for_red then
-    error "The \"/\" modifier should be put before any extra scope.";
+    user_err Pp.(str "The \"/\" modifier should be put before any extra scope.");
 
   let scopes_specified = List.exists Option.has_some scopes in
   
   if scopes_specified && clear_scopes_flag then
-    error "The \"clear scopes\" flag is incompatible with scope annotations.";
+    user_err Pp.(str "The \"clear scopes\" flag is incompatible with scope annotations.");
 
   let names = List.map (fun { name } -> name) args in
   let names = names :: List.map (List.map fst) more_implicits in
@@ -1062,7 +1062,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
     | name1 :: names1, name2 :: names2 ->
        if Name.equal name1 name2 then
          name1 :: names_union names1 names2
-       else error "Argument lists should agree on the names they provide."
+       else user_err Pp.(str "Argument lists should agree on the names they provide.")
   in
 
   let names = List.fold_left names_union [] names in
@@ -1143,10 +1143,10 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
   let implicits_specified = match implicits with [[]] -> false | _ -> true in
 
   if implicits_specified && clear_implicits_flag then
-    error "The \"clear implicits\" flag is incompatible with implicit annotations";
+    user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations");
 
   if implicits_specified && default_implicits_flag then
-    error "The \"default implicits\" flag is incompatible with implicit annotations";
+    user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations");
 
   let rargs =
     Util.List.map_filter (function (n, true) -> Some n | _ -> None)
@@ -1452,8 +1452,8 @@ let vernac_set_strategy locality l =
     match smart_global r with
       | ConstRef sp -> EvalConstRef sp
       | VarRef id -> EvalVarRef id
-      | _ -> error
-          "cannot set an inductive type or a constructor as transparent" in
+      | _ -> user_err Pp.(str
+          "cannot set an inductive type or a constructor as transparent") in
   let l = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) l in
   Redexpr.set_strategy local l
 
@@ -1463,8 +1463,8 @@ let vernac_set_opacity locality (v,l) =
     match smart_global r with
       | ConstRef sp -> EvalConstRef sp
       | VarRef id -> EvalVarRef id
-      | _ -> error
-          "cannot set an inductive type or a constructor as transparent" in
+      | _ -> user_err Pp.(str
+          "cannot set an inductive type or a constructor as transparent") in
   let l = List.map glob_ref l in
   Redexpr.set_strategy local [v,l]
 
@@ -1764,10 +1764,10 @@ let vernac_locate = let open Feedback in function
 
 let vernac_register id r =
  if Pfedit.refining () then
-    error "Cannot register a primitive while in proof editing mode.";
+    user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
   let t = (Constrintern.global_reference (snd id)) in
   if not (isConst t) then
-    error "Register inline: a constant is expected";
+    user_err Pp.(str "Register inline: a constant is expected");
   let kn = destConst t in
   match r with
   | RegisterInline -> Global.register_inline (Univ.out_punivs kn)
@@ -1780,7 +1780,7 @@ let vernac_focus gln =
     match gln with
       | None -> Proof.focus focus_command_cond () 1 p
       | Some 0 ->
-         CErrors.error "Invalid goal number: 0. Goal numbering starts with 1."
+         user_err Pp.(str "Invalid goal number: 0. Goal numbering starts with 1.")
       | Some n ->
          Proof.focus focus_command_cond () n p)
 
@@ -1795,7 +1795,7 @@ let vernac_unfocused () =
   if Proof.unfocused p then
     Feedback.msg_notice (str"The proof is indeed fully unfocused.")
   else
-    error "The proof is not fully unfocused."
+    user_err Pp.(str "The proof is not fully unfocused.")
 
 
 (* BeginSubproof / EndSubproof. 
@@ -2081,7 +2081,7 @@ let check_vernac_supports_locality c l =
     | VernacDeclareReduction _
     | VernacExtend _ 
     | VernacInductive _) -> ()
-  | Some _, _ -> CErrors.error "This command does not support Locality"
+  | Some _, _ -> user_err Pp.(str "This command does not support Locality")
 
 (* Vernaculars that take a polymorphism flag *)
 let check_vernac_supports_polymorphism c p =
@@ -2095,7 +2095,7 @@ let check_vernac_supports_polymorphism c p =
     | VernacInstance _ | VernacDeclareInstances _
     | VernacHints _ | VernacContext _
     | VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> ()
-  | Some _, _ -> CErrors.error "This command does not support Polymorphism"
+  | Some _, _ -> user_err Pp.(str "This command does not support Polymorphism")
 
 let enforce_polymorphism = function
   | None -> Flags.is_universe_polymorphism ()
@@ -2172,13 +2172,13 @@ let interp ?(verbosely=true) ?proof (loc,c) =
     | VernacStm _ -> assert false (* Done by Stm *)
 
     | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c
-    | VernacProgram _ -> CErrors.error "Program mode specified twice"
+    | VernacProgram _ -> user_err Pp.(str "Program mode specified twice")
     | VernacLocal (b, c) when Option.is_empty locality -> 
       aux ~locality:b ?polymorphism isprogcmd c
     | VernacPolymorphic (b, c) when polymorphism = None -> 
       aux ?locality ~polymorphism:b isprogcmd c
-    | VernacPolymorphic (b, c) -> CErrors.error "Polymorphism specified twice"
-    | VernacLocal _ -> CErrors.error "Locality specified twice"
+    | VernacPolymorphic (b, c) -> user_err Pp.(str "Polymorphism specified twice")
+    | VernacLocal _ -> user_err Pp.(str "Locality specified twice")
     | VernacFail v ->
         with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v)
     | VernacTimeout (n,v) ->