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

34 files changed, 98 insertions, 95 deletions

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 12d7f0660..b3ab29cce 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -53,9 +53,9 @@ let start_deriving f suchthat lemma =
           [suchthat], respectively. *)
       let (opaque,f_def,lemma_def) =
         match com with
-        | Admitted _ -> CErrors.error"Admitted isn't supported in Derive."
+        | Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.")
         | Proved (_,Some _,_) ->
-            CErrors.error"Cannot save a proof of Derive with an explicit name."
+            CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.")
         | Proved (opaque, None, obj) ->
             match Proof_global.(obj.entries) with
             | [_;f_def;lemma_def] ->
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 322fbcea7..2c85b185c 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -41,7 +41,7 @@ let toplevel_env () =
 	  | "MODULE TYPE" ->
             let modtype = Global.lookup_modtype (MPdot (mp, l)) in
             Some (l, SFBmodtype modtype)
-          | "INCLUDE" -> error "No extraction of toplevel Include yet."
+          | "INCLUDE" -> user_err Pp.(str "No extraction of toplevel Include yet.")
 	  | _ -> None
         end
     | _ -> None
@@ -435,7 +435,7 @@ let mono_filename f =
 	  else
             try Id.of_string (Filename.basename f)
 	    with UserError _ ->
-              error "Extraction: provided filename is not a valid identifier"
+              user_err Pp.(str "Extraction: provided filename is not a valid identifier")
 	in
 	Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 0692c88cd..b580fb592 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -185,7 +185,7 @@ let rec pp_expr par env args =
         pp_boxed_tuple (pp_expr true env []) l
     | MLcase (_,t, pv) when is_custom_match pv ->
         if not (is_regular_match pv) then
-	  error "Cannot mix yet user-given match and general patterns.";
+	  user_err Pp.(str "Cannot mix yet user-given match and general patterns.");
 	let mkfun (ids,_,e) =
 	  if not (List.is_empty ids) then named_lams (List.rev ids) e
 	  else dummy_lams (ast_lift 1 e) 1
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index d8e382155..4399fc561 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -246,7 +246,7 @@ let rec pp_expr par env args =
         pp_boxed_tuple (pp_expr true env []) l
     | MLcase (_, t, pv) when is_custom_match pv ->
         if not (is_regular_match pv) then
-	  error "Cannot mix yet user-given match and general patterns.";
+	  user_err Pp.(str "Cannot mix yet user-given match and general patterns.");
 	let mkfun (ids,_,e) =
 	  if not (List.is_empty ids) then named_lams (List.rev ids) e
 	  else dummy_lams (ast_lift 1 e) 1
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 8d0cc4a0d..3c81564e3 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -96,9 +96,9 @@ let rec pp_expr env args =
 		 prlist_with_sep spc (pp_cons_args env) args')
 	in
 	if is_coinductive r then paren (str "delay " ++ st) else st
-    | MLtuple _ -> error "Cannot handle tuples in Scheme yet."
+    | MLtuple _ -> user_err Pp.(str "Cannot handle tuples in Scheme yet.")
     | MLcase (_,_,pv) when not (is_regular_match pv) ->
-	error "Cannot handle general patterns in Scheme yet."
+	user_err Pp.(str "Cannot handle general patterns in Scheme yet.")
     | MLcase (_,t,pv) when is_custom_match pv ->
 	let mkfun (ids,_,e) =
 	  if not (List.is_empty ids) then named_lams (List.rev ids) e
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 5a1e7c26a..4c6355f61 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -161,7 +161,7 @@ let left_instance_tac (inst,id) continue seq=
 		  let evmap, _ =
 		    try Typing.type_of (pf_env gl) evmap gt
 		    with e when CErrors.noncritical e ->
-		      error "Untypable instance, maybe higher-order non-prenex quantification" in
+		      user_err Pp.(str "Untypable instance, maybe higher-order non-prenex quantification") in
 		    Sigma.Unsafe.of_pair (generalize [gt], evmap)
                 end })
 	    else
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 2d18b6605..826afc35b 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -227,7 +227,7 @@ let extend_with_auto_hints env sigma l seq =
       try
 	searchtable_map dbname
       with Not_found->
-	error ("Firstorder: "^dbname^" : No such Hint database") in
+	user_err Pp.(str ("Firstorder: "^dbname^" : No such Hint database")) in
       Hint_db.iter g hdb in
     List.iter h l;
     !seqref, sigma (*FIXME: forgetting about universes*)
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 25d8f8c83..f397f84a8 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -513,11 +513,11 @@ let rec fourier () =
 		        with NoIneq -> ())
               hyps;
     (* lineq = les inéquations découlant des hypothèses *)
-    if !lineq=[] then CErrors.error "No inequalities";
+    if !lineq=[] then CErrors.user_err Pp.(str "No inequalities");
     let res=fourier_lineq (!lineq) in
     let tac=ref (Proofview.tclUNIT ()) in
     if res=[]
-    then CErrors.error "fourier failed"
+    then CErrors.user_err Pp.(str "fourier failed")
     (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
     else (match res with
         [(cres,sres,lc)]->
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 55d361e3d..64f7813a3 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -820,10 +820,10 @@ let build_proof
 		      build_proof new_finalize {dyn_infos  with info = f } g
 	      end
 	  | Fix _ | CoFix _ ->
-	      error ( "Anonymous local (co)fixpoints are not handled yet")
+	      user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet"))
 
-	  | Proj _ -> error "Prod"
-	  | Prod _ -> error "Prod"
+	  | Proj _ -> user_err Pp.(str "Prod")
+	  | Prod _ -> user_err Pp.(str "Prod")
 	  | LetIn _ ->
 	      let new_infos =
 		{ dyn_infos with
@@ -1097,7 +1097,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	       (Global.env ())
 	       (Evd.empty)
 	       (EConstr.of_constr body)
-	| None -> error ( "Cannot define a principle over an axiom ")
+	| None -> user_err Pp.(str "Cannot define a principle over an axiom ")
     in
     let fbody = get_body fnames.(fun_num) in
     let f_ctxt,f_body = decompose_lam (project g) fbody in
@@ -1199,7 +1199,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 					 bs.(num),
 				       List.rev_map var_of_decl princ_params))
 				 ),num
-			 | _ -> error "Not a mutual block"
+			 | _ -> user_err Pp.(str "Not a mutual block")
 		   in
 		   let info =
 		     {infos with
@@ -1594,7 +1594,7 @@ let prove_principle_for_gen
   let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in
   let lemma =
     match !tcc_lemma_ref with
-     | Undefined -> error "No tcc proof !!"
+     | Undefined -> user_err Pp.(str "No tcc proof !!")
      | Value lemma -> EConstr.of_constr lemma
      | Not_needed -> EConstr.of_constr (Coqlib.build_coq_I ())
   in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 529b91c4c..18d63dd94 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -75,7 +75,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let rel_as_kn =
     fst (match princ_type_info.indref with
 	   | Some (Globnames.IndRef ind) -> ind
-	   | _ -> error "Not a valid predicate"
+	   | _ -> user_err Pp.(str "Not a valid predicate")
 	)
   in
   let ptes_vars = List.map Context.Named.Declaration.get_id new_predicates in
@@ -416,7 +416,7 @@ let get_funs_constant mp dp =
 	    in
 	    let body = EConstr.Unsafe.to_constr body in
 	    body
-	| None -> error ( "Cannot define a principle over an axiom ")
+	| None -> user_err Pp.(str ( "Cannot define a principle over an axiom "))
     in
     let f = find_constant_body const in
     let l_const = get_funs_constant const f in
@@ -432,7 +432,7 @@ let get_funs_constant mp dp =
       List.iter
 	(fun params ->
 	   if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && eq_constr c1 c2) first_params params)
-	   then error "Not a mutal recursive block"
+	   then user_err Pp.(str "Not a mutal recursive block")
 	)
 	l_params
     in
@@ -445,7 +445,7 @@ let get_funs_constant mp dp =
 	    | _ ->
 		if is_first && Int.equal (List.length l_bodies) 1
 		then raise Not_Rec
-		else error "Not a mutal recursive block"
+		else user_err Pp.(str "Not a mutal recursive block")
 	in
 	let first_infos = extract_info true (List.hd l_bodies) in
 	let check body  = (* Hope this is correct *)
@@ -454,7 +454,7 @@ let get_funs_constant mp dp =
             Array.equal eq_constr ta1 ta2 && Array.equal eq_constr ca1 ca2
 	  in
 	  if not (eq_infos first_infos (extract_info false body))
-	  then  error "Not a mutal recursive block"
+	  then  user_err Pp.(str "Not a mutal recursive block")
 	in
 	List.iter check l_bodies
       with Not_Rec -> ()
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 5e6128b1b..1db8be081 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -90,7 +90,7 @@ let pr_intro_as_pat _prc _ _ pat =
 
 let out_disjunctive = function
   | loc, IntroAction (IntroOrAndPattern l) -> (loc,l)
-  | _ -> CErrors.error "Disjunctive or conjunctive intro pattern expected."
+  | _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected.")
 
 ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat
 |   [ "as"  simple_intropattern(ipat) ] -> [ Some ipat ]
@@ -228,7 +228,7 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
 		  ;
 		    try Functional_principles_types.build_scheme fas
 		    with Functional_principles_types.No_graph_found ->
-		      CErrors.error ("Cannot generate induction principle(s)")
+		      CErrors.user_err Pp.(str "Cannot generate induction principle(s)")
 		      | e when CErrors.noncritical e ->
 			  let names = List.map (fun (_,na,_) -> na) fas in
 			  warning_error names e
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 7f2b21e79..d8614f376 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -576,8 +576,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 		   WARNING: We need to restart since [b] itself should be an application term
 		*)
 		build_entry_lc env funnames avoid (mkGApp(b,args))
-	    | GRec _ -> error "Not handled GRec"
-	    | GProd _ -> error "Cannot apply a type"
+	    | GRec _ -> user_err Pp.(str "Not handled GRec")
+	    | GProd _ -> user_err Pp.(str "Cannot apply a type")
 	end (* end of the application treatement *)
 
     | GLambda(n,_,t,b) ->
@@ -678,7 +678,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	  build_entry_lc env funnames avoid match_expr
 
 	end
-    | GRec _ -> error "Not handled GRec"
+    | GRec _ -> user_err Pp.(str "Not handled GRec")
     | GCast(b,_) ->
 	build_entry_lc env funnames  avoid b
 and build_entry_lc_from_case env funname make_discr
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 5abcb100f..0361e8cb1 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -120,7 +120,7 @@ let remove_name_from_mapping mapping na =
 
 let change_vars =
   let rec change_vars mapping rt =
-    CAst.map (function
+    CAst.map_with_loc (fun ?loc -> function
       | GRef _ as x -> x
       | GVar id ->
 	  let new_id =
@@ -172,7 +172,7 @@ let change_vars =
 	      change_vars mapping lhs,
 	      change_vars mapping rhs
 	     )
-      | GRec _ -> error "Local (co)fixes are not supported"
+      | GRec _ -> user_err ?loc Pp.(str "Local (co)fixes are not supported")
       | GSort _ as x -> x
       | GHole _ as x -> x
       | GCast(b,c) ->
@@ -352,7 +352,7 @@ let rec alpha_rt excluded rt =
 	    alpha_rt excluded lhs,
 	    alpha_rt excluded rhs
 	   )
-    | GRec _ -> error "Not handled GRec"
+    | GRec _ -> user_err Pp.(str "Not handled GRec")
     | GSort _
     | GHole _ as rt -> rt
     | GCast (b,c) ->
@@ -408,7 +408,7 @@ let is_free_in id =
 
     | GIf(cond,_,br1,br2) ->
 	is_free_in cond || is_free_in br1 || is_free_in br2
-    | GRec _ -> raise (UserError(None,str "Not handled GRec"))
+    | GRec _  -> user_err Pp.(str "Not handled GRec")
     | GSort _ -> false
     | GHole _ -> false
     | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
@@ -695,7 +695,7 @@ let expand_as =
       | GIf(e,(na,po),br1,br2) ->
 	  GIf(expand_as map e,(na,Option.map (expand_as map) po),
 	      expand_as map br1, expand_as map br2)
-      | GRec _ ->  error "Not handled GRec"
+      | GRec _ ->  user_err Pp.(str "Not handled GRec")
       | GCast(b,c) ->
 	  GCast(expand_as map b,
 		Miscops.map_cast_type (expand_as map) c)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index ab83cb15a..74c0eb4cc 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -186,6 +186,8 @@ let build_newrecursive l =
   in
   build_newrecursive l'
 
+let error msg = user_err Pp.(str msg)
+
 (* Checks whether or not the mutual bloc is recursive *)
 let is_rec names =
   let names = List.fold_right Id.Set.add names Id.Set.empty in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index ea985ddec..91dac303a 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -502,13 +502,13 @@ let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) =
        (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
 
 let decompose_lam_n sigma n =
-  if n < 0 then CErrors.error "decompose_lam_n: integer parameter must be positive";
+  if n < 0 then CErrors.user_err Pp.(str "decompose_lam_n: integer parameter must be positive");
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
     else match EConstr.kind sigma c with
       | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c
       | Cast (c,_,_)     -> lamdec_rec l n c
-      | _ -> CErrors.error "decompose_lam_n: not enough abstractions"
+      | _ -> CErrors.user_err Pp.(str "decompose_lam_n: not enough abstractions")
   in
   lamdec_rec [] n
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 8c972cd7c..8747efc02 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -197,7 +197,7 @@ let generate_type evd g_to_f f graph i =
 let find_induction_principle evd f =
   let f_as_constant,u =  match EConstr.kind !evd f with
     | Const c' -> c'
-    | _ -> error "Must be used with a function"
+    | _ -> user_err Pp.(str "Must be used with a function")
   in
   let infos = find_Function_infos f_as_constant in
   match infos.rect_lemma with
@@ -701,7 +701,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
       let graph_def = graphs.(j) in
       let infos =
         try find_Function_infos (fst (destConst (project g) funcs.(j)))
-        with Not_found ->  error "No graph found"
+        with Not_found ->  user_err Pp.(str "No graph found")
       in
       if infos.is_general
         || Rtree.is_infinite Declareops.eq_recarg graph_def.mind_recargs
@@ -1006,6 +1006,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
       | _ -> tclFAIL 1 (mt ()) g
 
 
+let error msg = user_err Pp.(str msg)
 
 let invfun qhyp f  =
   let f =
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index b99a05dfb..b2c8489ce 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -347,7 +347,7 @@ let filter_shift_stable_right (lnk:int merged_arg array) (l:'a list): 'a list =
   filter_shift_stable lnk (Array.to_list larr)
 
 
-
+let error msg = user_err Pp.(str msg)
 
 (** {1 Utilities for merging} *)
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index c46309355..e206955ac 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -136,7 +136,7 @@ let ex = function () -> (coq_init_constant "ex")
 let nat = function () -> (coq_init_constant "nat")
 let iter_ref () =  
   try find_reference ["Recdef"] "iter" 
-  with Not_found -> error "module Recdef not loaded"
+  with Not_found -> user_err Pp.(str "module Recdef not loaded")
 let iter = function () -> (constr_of_global (delayed_force iter_ref))
 let eq = function () -> (coq_init_constant "eq")
 let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
@@ -323,8 +323,8 @@ let check_not_nested sigma forbidden e =
       | Construct _ -> ()
       | Case(_,t,e,a) -> 
 	check_not_nested t;check_not_nested e;Array.iter check_not_nested a
-      | Fix _ -> error "check_not_nested : Fix"
-      | CoFix _ -> error "check_not_nested : Fix"
+      | Fix _ -> user_err Pp.(str "check_not_nested : Fix")
+      | CoFix _ -> user_err Pp.(str "check_not_nested : Fix")
   in
   try 
     check_not_nested e 
@@ -430,8 +430,8 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
 let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
   let sigma = project g in
   match EConstr.kind sigma expr_info.info with 
-    | CoFix _ | Fix _ -> error "Function cannot treat local fixpoint or cofixpoint"
-    | Proj _ -> error "Function cannot treat projections"
+    | CoFix _ | Fix _ -> user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint")
+    | Proj _ -> user_err Pp.(str "Function cannot treat projections")
     | LetIn(na,b,t,e) -> 
       begin
 	let new_continuation_tac = 
@@ -1304,7 +1304,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
   in
   let na = next_global_ident_away name [] in
   if Termops.occur_existential sigma gls_type then
-    CErrors.error "\"abstract\" cannot handle existentials";
+    CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials");
   let hook _ _ =
     let opacity =
       let na_ref = Libnames.Ident (Loc.tag na) in
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 470a93f2b..bf84f61a5 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -56,17 +56,16 @@ let instantiate_tac n c ido =
 		InHyp ->
 		  (match decl with
                     | LocalAssum (_,typ) -> evar_list sigma (EConstr.of_constr typ)
-		    | _ -> error
-			"Please be more specific: in type or value?")
+		    | _ -> user_err Pp.(str "Please be more specific: in type or value?"))
 	      | InHypTypeOnly ->
 		  evar_list sigma (EConstr.of_constr (NamedDecl.get_type decl))
 	      | InHypValueOnly ->
 		  (match decl with
 		    | LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body)
-		    | _ -> error "Not a defined hypothesis.") in
+		    | _ -> user_err Pp.(str "Not a defined hypothesis.")) in
   if List.length evl < n then
-    error "Not enough uninstantiated existential variables.";
-  if n <= 0 then error "Incorrect existential variable index.";
+    user_err Pp.(str "Not enough uninstantiated existential variables.");
+  if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
   let evk,_ = List.nth evl (n-1) in
   instantiate_evar evk c sigma gl
   end
@@ -76,7 +75,7 @@ let instantiate_tac_by_name id c =
   let sigma = gl.sigma in
   let evk =
     try Evd.evar_key id sigma
-    with Not_found -> error "Unknown existential variable." in
+    with Not_found -> user_err Pp.(str "Unknown existential variable.") in
   instantiate_evar evk c sigma gl
   end
 
@@ -109,8 +108,8 @@ let hget_evar n =
   let concl = Proofview.Goal.concl gl in
   let evl = evar_list sigma concl in
   if List.length evl < n then
-    error "Not enough uninstantiated existential variables.";
-  if n <= 0 then error "Incorrect existential variable index.";
+    user_err Pp.(str "Not enough uninstantiated existential variables.");
+  if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
   let ev = List.nth evl (n-1) in
   let ev_type = EConstr.existential_type sigma ev in
   Tactics.change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl))
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index a3310c2d8..fdb8d3461 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -90,7 +90,7 @@ let occurrences_of = function
   | n::_ as nl when n < 0 -> AllOccurrencesBut (List.map abs nl)
   | nl ->
       if List.exists (fun n -> n < 0) nl then
-        CErrors.error "Illegal negative occurrence number.";
+        CErrors.user_err Pp.(str "Illegal negative occurrence number.");
       OnlyOccurrences nl
 
 let coerce_to_int v = match Value.to_int v with
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index cbd8a7f0f..ed80dd7ae 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -1084,7 +1084,7 @@ let decompose l c =
     let sigma = Tacmach.New.project gl in
     let to_ind c =
       if isInd sigma c then fst (destInd sigma c)
-      else error "not an inductive type"
+      else user_err Pp.(str "not an inductive type")
     in
     let l = List.map to_ind l in
     Elim.h_decompose l c
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 257100b01..1404b1c1f 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -117,8 +117,8 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
       | _, Some x ->
           let ids = List.map snd (List.flatten (List.map pi1 bl)) in
           (try List.index Names.Name.equal (snd x) ids
-          with Not_found -> error "No such fix variable.")
-      | _ -> error "Cannot guess decreasing argument of fix." in
+          with Not_found -> user_err Pp.(str "No such fix variable."))
+      | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in
   (id,n, CAst.make ~loc @@ CProdN(bl,ty))
 
 let mk_cofix_tac (loc,id,bl,ann,ty) =
@@ -152,7 +152,7 @@ let mkTacCase with_evar = function
   | ic ->
       if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic)
       then
-	error "Use of numbers as direct arguments of 'case' is not supported.";
+	user_err Pp.(str "Use of numbers as direct arguments of 'case' is not supported.");
       TacInductionDestruct (false,with_evar,ic)
 
 let rec mkCLambdaN_simple_loc ?loc bll c =
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 75ab1c5ee..a001c6a2b 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -348,7 +348,7 @@ type 'a extra_genarg_printer =
             let bll = List.map (fun (x, _, y) -> x, y) bll in
             if nb >= n then (List.rev (bll@acc)), a
             else strip_ty (bll@acc) (n-nb) a
-        | _ -> error "Cannot translate fix tactic: not enough products" in
+        | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
     strip_ty [] n ty
 
   let pr_ltac_or_var pr = function
@@ -1089,7 +1089,7 @@ type 'a extra_genarg_printer =
         match ty.CAst.v with
             Glob_term.GProd(na,Explicit,a,b) ->
               strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b
-          | _ -> error "Cannot translate fix tactic: not enough products" in
+          | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
     strip_ty [] n ty
 
   let raw_printers =
@@ -1160,7 +1160,7 @@ type 'a extra_genarg_printer =
         match Term.kind_of_term ty with
             Term.Prod(na,a,b) ->
               strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
-          | _ -> error "Cannot translate fix tactic: not enough products" in
+          | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
     strip_ty [] n ty
 
   let pr_atomic_tactic_level env sigma n t =
@@ -1210,7 +1210,7 @@ let declare_extra_genarg_pprule wit
   (h : 'c extra_genarg_printer) =
   begin match wit with
     | ExtraArg s -> ()
-    | _          -> error "Can declare a pretty-printing rule only for extra argument types."
+    | _          -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.")
   end;
   let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in
   let g x =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index e8c9f4eba..51729f4c6 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -241,7 +241,7 @@ end) = struct
 	    let liftarg = mkLambda (na, ty, arg) in
 	    let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in
 	      if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
-	      else error "build_signature: no constraint can apply on a dependent argument"
+	      else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument")
 	| _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products")
 	| _, [] ->
 	  (match finalcstr with
@@ -478,7 +478,7 @@ type hypinfo = {
 let get_symmetric_proof b = 
   if b then PropGlobal.get_symmetric_proof else TypeGlobal.get_symmetric_proof
 
-let error_no_relation () = error "Cannot find a relation to rewrite."
+let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite.")
 
 let rec decompose_app_rel env evd t = 
   (** Head normalize for compatibility with the old meta mechanism *)
@@ -531,7 +531,7 @@ let decompose_applied_relation env sigma (c,l) =
 	let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *)
 	match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with
 	| Some c -> c
-	| None -> error "Cannot find an homogeneous relation to rewrite."
+	| None -> user_err Pp.(str "Cannot find an homogeneous relation to rewrite.")
 
 let rewrite_db = "rewrite"
 
@@ -837,7 +837,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
 	      sigargs, r.rew_to :: typeargs')
 	  | None ->
 	      if not (Option.is_empty y) then 
-		error "Cannot rewrite inside dependent arguments of a function";
+		user_err Pp.(str "Cannot rewrite inside dependent arguments of a function");
 	      x :: acc, x :: subst, evars, sigargs, x :: typeargs')
       ([], [], evars, sigargs, []) args args'
   in
@@ -1425,7 +1425,7 @@ module Strategies =
 	let unfolded =
 	  try Tacred.try_red_product env sigma c
 	  with e when CErrors.noncritical e ->
-            error "fold: the term is not unfoldable !"
+            user_err Pp.(str "fold: the term is not unfoldable !")
 	in
 	  try
 	    let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in
@@ -2204,7 +2204,7 @@ let setoid_symmetry_in id =
   let rec split_last_two = function
     | [c1;c2] -> [],(c1, c2)
     | x::y::z -> let l,res = split_last_two (y::z) in x::l, res
-    | _ -> error "Cannot find an equivalence relation to rewrite."
+    | _ -> user_err Pp.(str "Cannot find an equivalence relation to rewrite.")
   in
   let others,(c1,c2) = split_last_two args in
   let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 4d7b0f929..75f89a81e 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -60,7 +60,7 @@ let get_tacentry n m =
   else EntryName (rawwit Tacarg.wit_tactic, atactic n)
 
 let get_separator = function
-| None -> error "Missing separator."
+| None -> user_err Pp.(str "Missing separator.")
 | Some sep -> sep
 
 let rec parse_user_entry s sep =
@@ -110,7 +110,7 @@ let get_tactic_entry n =
   else if 1<=n && n<5 then
     Pltac.tactic_expr, Some (Extend.Level (string_of_int n))
   else
-    error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
+    user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^"."))
 
 (**********************************************************************)
 (** State of the grammar extensions                                   *)
@@ -170,7 +170,7 @@ let add_tactic_entry (kn, ml, tg) state =
   in
   let () =
     if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
-      error "Notation for simple tactic must start with an identifier."
+      user_err Pp.(str "Notation for simple tactic must start with an identifier.")
   in
   let map = function
   | TacTerm s -> GramTerminal s
@@ -208,7 +208,7 @@ let interp_prod_item = function
     | None ->
       if String.Map.mem s !entry_names then String.Map.find s !entry_names
       else begin match ArgT.name s with
-      | None -> error ("Unknown entry "^s^".")
+      | None -> user_err Pp.(str ("Unknown entry "^s^"."))
       | Some arg -> arg
       end
     | Some n ->
@@ -253,8 +253,8 @@ let pprule pa = {
 
 let check_key key =
   if Tacenv.check_alias key then
-    error "Conflicting tactic notations keys. This can happen when including \
-    twice the same module."
+    user_err Pp.(str "Conflicting tactic notations keys. This can happen when including \
+    twice the same module.")
 
 let cache_tactic_notation (_, tobj) =
   let key = tobj.tacobj_key in
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 6c7eb8c89..e431a13bc 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -252,7 +252,7 @@ and intern_or_and_intro_pattern lf ist = function
 let intern_or_and_intro_pattern_loc lf ist = function
   | ArgVar (_,id) as x ->
       if find_var id ist then x
-      else error "Disjunctive/conjunctive introduction pattern expected."
+      else user_err Pp.(str "Disjunctive/conjunctive introduction pattern expected.")
   | ArgArg (loc,l) -> ArgArg (loc,intern_or_and_intro_pattern lf ist l)
 
 let intern_intro_pattern_naming_loc lf ist (loc,pat) =
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 632b9dac1..af8107025 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -462,7 +462,7 @@ let theoremedeszeros_termes lp =
 	  lexico:=true;
       |7 -> sinfo "ordre lexico computation with sugar, division by pairs";
 	  lexico:=true;
-      | _ -> error "nsatz: bad parameter"
+      | _ -> user_err Pp.(str "nsatz: bad parameter")
        );
       let lvar = List.init nvars (fun i -> Printf.sprintf "x%i" (i + 1)) in
       let lvar = ["a";"b";"c";"d";"e";"f";"g";"h";"i";"j";"k";"l";"m";"n";"o";"p";"q";"r";"s";"t";"u";"v";"w";"x";"y";"z"] @ lvar in
@@ -549,5 +549,5 @@ let nsatz_compute t =
   let lpol =
     try nsatz t
     with Ideal.NotInIdeal ->
-      error "nsatz cannot solve this problem" in
+      user_err Pp.(str "nsatz cannot solve this problem") in
   return_term lpol
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 334baec8d..d3ca874bd 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -456,7 +456,7 @@ let destructurate_prop sigma t =
 	Kapp (Other (string_of_path (path_of_global (IndRef isp))),args)
     | Var id,[] -> Kvar id
     | Prod (Anonymous,typ,body), [] -> Kimp(typ,body)
-    | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal"
+    | Prod (Name _,_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal")
     | _ -> Kufo
 
 let destructurate_type sigma t =
@@ -891,7 +891,7 @@ let rec scalar p n = function
          (Lazy.force coq_fast_Zmult_assoc_reverse);
        focused_simpl (P_APP 2 :: p)],
       Otimes(t1,Oz (n*x))
-  | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products"
+  | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products")
   | (Oatom _ as t) -> [], Otimes(t,Oz n)
   | Oz i -> [focused_simpl p],Oz(n*i)
   | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n; c |]))
@@ -943,7 +943,7 @@ let rec negate p = function
       [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]]
          (Lazy.force coq_fast_Zopp_mult_distr_r);
        focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (neg x))
-  | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products"
+  | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products")
   | (Oatom _ as t) ->
       let r = Otimes(t,Oz(negone)) in
       [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1)], r
@@ -1026,7 +1026,7 @@ let shrink_pair p f1 f2 =
     | t1,t2 ->
 	begin
 	  oprint t1; print_newline (); oprint t2; print_newline ();
-	  flush Pervasives.stdout; error "shrink.1"
+	  flush Pervasives.stdout; CErrors.user_err Pp.(str "shrink.1")
 	end
 
 let reduce_factor p = function
@@ -1038,10 +1038,10 @@ let reduce_factor p = function
       let rec compute = function
         | Oz n -> n
 	| Oplus(t1,t2) -> Bigint.add (compute t1) (compute t2)
-	| _ -> error "condense.1"
+	| _ -> CErrors.user_err Pp.(str "condense.1")
       in
       [focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c))
-  | t -> oprint t; error "reduce_factor.1"
+  | t -> oprint t; CErrors.user_err Pp.(str "reduce_factor.1")
 
 let rec condense p = function
   | Oplus(f1,(Oplus(f2,r) as t)) ->
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 6b711a176..ce7ffb1e7 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -35,7 +35,7 @@ let omega_tactic l =
        | "positive" -> eval_tactic "zify_positive"
        | "N" -> eval_tactic "zify_N"
        | "Z" -> eval_tactic "zify_op"
-       | s -> CErrors.error ("No Omega knowledge base for type "^s))
+       | s -> CErrors.user_err Pp.(str ("No Omega knowledge base for type "^s)))
     (Util.List.sort_uniquize String.compare l)
   in
   Tacticals.New.tclTHEN
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index c649cfb2c..db69f1b40 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -183,7 +183,7 @@ type inversion_scheme = {
   goal [gl]. This function uses the auxiliary functions
   [i_can't_do_that], [decomp_term], [compute_lhs] and [compute_rhs]. *)
 
-let i_can't_do_that () = error "Quote: not a simple fixpoint"
+let i_can't_do_that () = user_err Pp.(str "Quote: not a simple fixpoint")
 
 let decomp_term sigma c = EConstr.kind sigma (Termops.strip_outer_cast sigma c)
 
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index c2d7d5050..6479c683b 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -28,7 +28,7 @@ let romega_tactic unsafe l =
        | "positive" -> eval_tactic "zify_positive"
        | "N" -> eval_tactic "zify_N"
        | "Z" -> eval_tactic "zify_op"
-       | s -> CErrors.error ("No ROmega knowledge base for type "^s))
+       | s -> CErrors.user_err Pp.(str ("No ROmega knowledge base for type "^s)))
     (Util.List.sort_uniquize String.compare l)
   in
   Tacticals.New.tclTHEN
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index e56605076..fdcd62299 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1042,5 +1042,5 @@ let total_reflexive_omega_tactic unsafe =
   let systems_list = destructurate_hyps full_reified_goal in
   if !debug then display_systems systems_list;
   resolution unsafe env reified_goal systems_list
-  with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system"
+  with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system")
   end }
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e20e78b1a..0e1225ada 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -8,7 +8,6 @@
 
 open Ltac_plugin
 open Pp
-open CErrors
 open Util
 open Names
 open Term
@@ -32,6 +31,8 @@ open Misctypes
 open Newring_ast
 open Proofview.Notations
 
+let error msg = CErrors.user_err Pp.(str msg)
+
 (****************************************************************************)
 (* controlled reduction *)
 
@@ -46,7 +47,7 @@ let tag_arg tag_rec map subs i c =
 let global_head_of_constr sigma c = 
   let f, args = decompose_app sigma c in
     try fst (Termops.global_of_constr sigma f)
-    with Not_found -> anomaly (str "global_head_of_constr")
+    with Not_found -> CErrors.anomaly (str "global_head_of_constr")
 
 let global_of_constr_nofail c = 
   try global_of_constr c
@@ -82,7 +83,7 @@ let add_map s m = protect_maps := String.Map.add s m !protect_maps
 let lookup_map map =
   try String.Map.find map !protect_maps
   with Not_found ->
-    user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found")
+    CErrors.user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found")
 
 let protect_red map env sigma c0 =
   let evars ev = Evarutil.safe_evar_value sigma ev in
@@ -359,13 +360,13 @@ let find_ring_structure env sigma l =
         let check c =
           let ty' = Retyping.get_type_of env sigma c in
           if not (Reductionops.is_conv env sigma ty ty') then
-            user_err ~hdr:"ring"
+            CErrors.user_err ~hdr:"ring"
               (str"arguments of ring_simplify do not have all the same type")
         in
         List.iter check cl';
         (try ring_for_carrier (EConstr.to_constr sigma ty)
         with Not_found ->
-          user_err ~hdr:"ring"
+          CErrors.user_err ~hdr:"ring"
             (str"cannot find a declared ring structure over"++
              spc()++str"\""++pr_constr ty++str"\""))
     | [] -> assert false
@@ -852,13 +853,13 @@ let find_field_structure env sigma l =
         let check c =
           let ty' = Retyping.get_type_of env sigma c in
           if not (Reductionops.is_conv env sigma ty ty') then
-            user_err ~hdr:"field"
+            CErrors.user_err ~hdr:"field"
               (str"arguments of field_simplify do not have all the same type")
         in
         List.iter check cl';
         (try field_for_carrier (EConstr.to_constr sigma ty)
         with Not_found ->
-          user_err ~hdr:"field"
+          CErrors.user_err ~hdr:"field"
             (str"cannot find a declared field structure over"++
              spc()++str"\""++pr_constr ty++str"\""))
     | [] -> assert false
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 862e44cca..6b752fb4b 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -468,7 +468,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p =
     | Evar (k, _) ->
       if Evd.mem sigma0 k then KpatEvar k, f, a else
       if a <> [] then KpatFlex, f, a else 
-      (match p_origin with None -> CErrors.error "indeterminate pattern"
+      (match p_origin with None -> CErrors.user_err Pp.(str "indeterminate pattern")
       | Some (dir, rule) ->
 	errorstrm (str "indeterminate " ++ pr_dir_side dir
           ++ str " in " ++ pr_constr_pat rule))
@@ -1320,7 +1320,7 @@ let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h =
 let fill_occ_term env cl occ sigma0 (sigma, t) =
   try
     let sigma',uc,t',cl,_= pf_fill_occ env cl occ sigma0 t (sigma, t) all_ok 1 in
-    if sigma' != sigma0 then CErrors.error "matching impacts evars"
+    if sigma' != sigma0 then CErrors.user_err Pp.(str "matching impacts evars")
     else cl, (Evd.merge_universe_context sigma' uc, t')
   with NoMatch -> try
     let sigma', uc, t' =