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

10 files changed, 35 insertions, 32 deletions

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