From de038270f72214b169d056642eb7144a79e6f126 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 7 Jul 2016 04:56:24 +0200
Subject: Unify location handling of error functions.

In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.

We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.

This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
---
 pretyping/cases.ml           | 44 ++++++++++++------------
 pretyping/cases.mli          |  4 +--
 pretyping/coercion.ml        |  8 ++---
 pretyping/detyping.ml        |  8 ++---
 pretyping/evarconv.ml        |  4 +--
 pretyping/evardefine.ml      |  4 +--
 pretyping/patternops.ml      | 14 ++++----
 pretyping/pretype_errors.ml  | 80 +++++++++++++++++++++-----------------------
 pretyping/pretype_errors.mli | 53 ++++++++++++++---------------
 pretyping/pretyping.ml       | 66 ++++++++++++++++++------------------
 10 files changed, 138 insertions(+), 147 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 447a4c487c..85c518019e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -45,22 +45,22 @@ type pattern_matching_error =
 
 exception PatternMatchingError of env * evar_map * pattern_matching_error
 
-let raise_pattern_matching_error (loc,env,sigma,te) =
-  Loc.raise loc (PatternMatchingError(env,sigma,te))
+let raise_pattern_matching_error ?loc (env,sigma,te) =
+  Loc.raise ?loc (PatternMatchingError(env,sigma,te))
 
-let error_bad_pattern_loc loc env sigma cstr ind =
-  raise_pattern_matching_error
-    (loc, env, sigma, BadPattern (cstr,ind))
+let error_bad_pattern ?loc env sigma cstr ind =
+  raise_pattern_matching_error ?loc
+    (env, sigma, BadPattern (cstr,ind))
 
-let error_bad_constructor_loc loc env cstr ind =
+let error_bad_constructor ?loc env cstr ind =
   raise_pattern_matching_error
-    (loc, env, Evd.empty, BadConstructor (cstr,ind))
+    (env, Evd.empty, BadConstructor (cstr,ind))
 
-let error_wrong_numarg_constructor_loc loc env c n =
-  raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargConstructor(c,n))
+let error_wrong_numarg_constructor ?loc env c n =
+  raise_pattern_matching_error (env, Evd.empty, WrongNumargConstructor(c,n))
 
-let error_wrong_numarg_inductive_loc loc env c n =
-  raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargInductive(c,n))
+let error_wrong_numarg_inductive ?loc env c n =
+  raise_pattern_matching_error (env, Evd.empty, WrongNumargInductive(c,n))
 
 let rec list_try_compile f = function
   | [a] -> f a
@@ -479,26 +479,25 @@ let check_and_adjust_constructor env ind cstrs = function
 	    let args' = adjust_local_defs loc (args, List.rev ci.cs_args)
 	    in PatCstr (loc, cstr, args', alias)
 	  with NotAdjustable ->
-	    error_wrong_numarg_constructor_loc loc env cstr nb_args_constr
+	    error_wrong_numarg_constructor ~loc env cstr nb_args_constr
       else
 	(* Try to insert a coercion *)
 	try
 	  Coercion.inh_pattern_coerce_to loc env pat ind' ind
 	with Not_found ->
-	  error_bad_constructor_loc loc env cstr ind
+	  error_bad_constructor ~loc env cstr ind
 
 let check_all_variables env sigma typ mat =
   List.iter
     (fun eqn -> match current_pattern eqn with
        | PatVar (_,id) -> ()
        | PatCstr (loc,cstr_sp,_,_) ->
-	   error_bad_pattern_loc loc env sigma cstr_sp typ)
+	   error_bad_pattern ~loc env sigma cstr_sp typ)
     mat
 
 let check_unused_pattern env eqn =
   if not !(eqn.used) then
-    raise_pattern_matching_error
-      (eqn.eqn_loc, env, Evd.empty, UnusedClause eqn.patterns)
+    raise_pattern_matching_error ~loc:eqn.eqn_loc (env, Evd.empty, UnusedClause eqn.patterns)
 
 let set_used_pattern eqn = eqn.used := true
 
@@ -1305,8 +1304,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
   let submat = adjust_impossible_cases pb pred tomatch submat in
   let () = match submat with
   | [] ->
-    raise_pattern_matching_error
-      (Loc.ghost, pb.env, Evd.empty, NonExhaustive (complete_history history))
+    raise_pattern_matching_error (pb.env, Evd.empty, NonExhaustive (complete_history history))
   | _ -> ()
   in
 
@@ -1834,8 +1832,8 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 		       | None -> [LocalAssum (na, lift n typ)]
 		       | Some b -> [LocalDef (na, lift n b, lift n typ)])
 	    | Some (loc,_,_) ->
- 	    user_err_loc (loc,"",
-	    str"Unexpected type annotation for a term of non inductive type."))
+ 	    user_err ~loc ""
+                (str"Unexpected type annotation for a term of non inductive type."))
       | IsInd (term,IndType(indf,realargs),_) ->
           let indf' = if dolift then lift_inductive_family n indf else indf in
 	  let ((ind,u),_) = dest_ind_family indf' in
@@ -1845,7 +1843,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 	    match t with
 	      | Some (loc,ind',realnal) ->
 		  if not (eq_ind ind ind') then
-		    user_err_loc (loc,"",str "Wrong inductive type.");
+		    user_err ~loc "" (str "Wrong inductive type.");
 		  if not (Int.equal nrealargs_ctxt (List.length realnal)) then
 		      anomaly (Pp.str "Ill-formed 'in' clause in cases");
 		  List.rev realnal
@@ -2036,11 +2034,11 @@ let constr_of_pat env evdref arsign pat avoid =
 	let cind = inductive_of_constructor cstr in
 	let IndType (indf, _) = 
 	  try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty)
-	  with Not_found -> error_case_not_inductive env 
+	  with Not_found -> error_case_not_inductive env !evdref
 	    {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty}
 	in
 	let (ind,u), params = dest_ind_family indf in
-	if not (eq_ind ind cind) then error_bad_constructor_loc l env cstr ind;
+	if not (eq_ind ind cind) then error_bad_constructor ~loc:l env cstr ind;
 	let cstrs = get_constructors env indf in
 	let ci = cstrs.(i-1) in
 	let nb_args_constr = ci.cs_nargs in
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index ba566f3744..6bc61f6dda 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -28,9 +28,9 @@ type pattern_matching_error =
 
 exception PatternMatchingError of env * evar_map * pattern_matching_error
 
-val error_wrong_numarg_constructor_loc : Loc.t -> env -> constructor -> int -> 'a
+val error_wrong_numarg_constructor : ?loc:Loc.t -> env -> constructor -> int -> 'a
 
-val error_wrong_numarg_inductive_loc : Loc.t -> env -> inductive -> int -> 'a
+val error_wrong_numarg_inductive   : ?loc:Loc.t -> env -> inductive -> int -> 'a
 
 val irrefutable : env -> cases_pattern -> bool
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 913e80f399..98dea9fc9a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -412,7 +412,7 @@ let inh_tosort_force loc env evd j =
     let j2 = on_judgment_type (whd_evar evd) j1 in
       (evd,type_judgment env j2)
   with Not_found | NoCoercion ->
-    error_not_a_type_loc loc env evd j
+    error_not_a_type ~loc env evd j
 
 let inh_coerce_to_sort loc env evd j =
   let typ = whd_all env evd j.uj_type in
@@ -506,16 +506,16 @@ let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t =
 	else raise NoSubtacCoercion
       with
       | NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion ->
-	  error_actual_type_loc loc env best_failed_evd cj t e
+	  error_actual_type ~loc env best_failed_evd cj t e
       | NoSubtacCoercion ->
 	let evd' = saturate_evd env evd in
       	  try
 	    if evd' == evd then 
-	      error_actual_type_loc loc env best_failed_evd cj t e
+	      error_actual_type ~loc env best_failed_evd cj t e
 	    else 
       	      inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t
 	  with NoCoercionNoUnifier (_evd,_error) ->
-	    error_actual_type_loc loc env best_failed_evd cj t e
+	    error_actual_type ~loc env best_failed_evd cj t e
   in
   let val' = match val' with Some v -> v | None -> assert(false) in
     (evd',{ uj_val = val'; uj_type = t })
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 85125a502e..ab93939150 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -67,15 +67,15 @@ let isomorphic_to_tuple lc = Int.equal (Array.length lc) 1
 let encode_bool r =
   let (x,lc) = encode_inductive r in
   if not (has_two_constructors lc) then
-    user_err_loc (loc_of_reference r,"encode_if",
-      str "This type has not exactly two constructors.");
+    user_err ~loc:(loc_of_reference r) "encode_if"
+      (str "This type has not exactly two constructors.");
   x
 
 let encode_tuple r =
   let (x,lc) = encode_inductive r in
   if not (isomorphic_to_tuple lc) then
-    user_err_loc (loc_of_reference r,"encode_tuple",
-      str "This type cannot be seen as a tuple type.");
+    user_err ~loc:(loc_of_reference r) "encode_tuple"
+      (str "This type cannot be seen as a tuple type.");
   x
 
 module PrintingInductiveMake =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0fea2ba223..26af90958b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1249,7 +1249,7 @@ let consider_remaining_unif_problems env
 	      aux evd pbs progress (pb :: stuck)
             end
         | UnifFailure (evd,reason) ->
-	    Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb)
+	    Pretype_errors.error_cannot_unify ~loc:(loc_of_conv_pb evd pb)
               env evd ~reason (t1, t2))
     | _ -> 
 	if progress then aux evd stuck false []
@@ -1258,7 +1258,7 @@ let consider_remaining_unif_problems env
 	  | [] -> (* We're finished *) evd
 	  | (pbty,env,t1,t2 as pb) :: _ ->
 	      (* There remains stuck problems *)
-	      Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb)
+	      Pretype_errors.error_cannot_unify ~loc:(loc_of_conv_pb evd pb)
                 env evd (t1, t2)
   in
   let (evd,pbs) = extract_all_conv_pbs evd in
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index f9ab75cea9..b91ae6c724 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -135,7 +135,7 @@ let define_pure_evar_as_lambda env evd evk =
   let evd1,(na,dom,rng) = match kind_of_term typ with
   | Prod (na,dom,rng) -> (evd,(na,dom,rng))
   | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ
-  | _ -> error_not_product_loc Loc.ghost env evd typ in
+  | _ -> error_not_product env evd typ in
   let avoid = ids_of_named_context (evar_context evi) in
   let id =
     next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in
@@ -191,7 +191,7 @@ let split_tycon loc env evd tycon =
 	| App (c,args) when isEvar c ->
 	    let (evd',lam) = define_evar_as_lambda env evd (destEvar c) in
 	    real_split evd' (mkApp (lam,args))
-	| _ -> error_not_product_loc loc env evd c
+	| _ -> error_not_product ~loc env evd c
   in
     match tycon with
       | None -> evd,(Anonymous,None,None)
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index fe73b6105b..99c3772db9 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -315,7 +315,7 @@ let rec subst_pattern subst pat =
 let mkPLambda na b = PLambda(na,PMeta None,b)
 let rev_it_mkPLambda = List.fold_right mkPLambda
 
-let err loc pp = user_err_loc (loc,"pattern_of_glob_constr", pp)
+let err ?loc pp = user_err ?loc "pattern_of_glob_constr" pp
 
 let warn_cast_in_pattern =
   CWarnings.create ~name:"cast-in-pattern" ~category:"automation"
@@ -387,7 +387,7 @@ let rec pat_of_raw metas vars = function
           rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
         | (None | Some (GHole _)), _ -> PMeta None
 	| Some p, None ->
-            user_err_loc (loc,"",strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
+            user_err ~loc "" (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
       in
       let info =
 	{ cip_style = sty;
@@ -400,12 +400,12 @@ let rec pat_of_raw metas vars = function
 	 one non-trivial branch. These facts are used in [Constrextern]. *)
       PCase (info, pred, pat_of_raw metas vars c, brs)
 
-  | r -> err (loc_of_glob_constr r) (Pp.str "Non supported pattern.")
+  | r -> err ~loc:(loc_of_glob_constr r) (Pp.str "Non supported pattern.")
 
 and pats_of_glob_branches loc metas vars ind brs =
   let get_arg = function
     | PatVar(_,na) -> na
-    | PatCstr(loc,_,_,_) -> err loc (Pp.str "Non supported pattern.")
+    | PatCstr(loc,_,_,_) -> err ~loc (Pp.str "Non supported pattern.")
   in
   let rec get_pat indexes = function
     | [] -> false, []
@@ -414,10 +414,10 @@ and pats_of_glob_branches loc metas vars ind brs =
       let () = match ind with
       | Some sp when eq_ind sp indsp -> ()
       | _ ->
-        err loc (Pp.str "All constructors must be in the same inductive type.")
+        err ~loc (Pp.str "All constructors must be in the same inductive type.")
       in
       if Int.Set.mem (j-1) indexes then
-	err loc
+	err ~loc
           (str "No unique branch for " ++ int j ++ str"-th constructor.");
       let lna = List.map get_arg lv in
       let vars' = List.rev lna @ vars in
@@ -425,7 +425,7 @@ and pats_of_glob_branches loc metas vars ind brs =
       let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in
       let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in
       ext, ((j-1, tags, pat) :: pats)
-    | (loc,_,_,_) :: _ -> err loc (Pp.str "Non supported pattern.")
+    | (loc,_,_,_) :: _ -> err ~loc (Pp.str "Non supported pattern.")
   in
   get_pat Int.Set.empty brs
 
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 00b6100c02..5b09586950 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -64,43 +64,42 @@ let precatchable_exception = function
   | Nametab.GlobalizationError _ -> true
   | _ -> false
 
-let raise_pretype_error (loc,env,sigma,te) =
-  Loc.raise loc (PretypeError(env,sigma,te))
+let raise_pretype_error ?loc (env,sigma,te) =
+  Loc.raise ?loc (PretypeError(env,sigma,te))
 
-let raise_located_type_error (loc,env,sigma,te) =
-  Loc.raise loc (PretypeError(env,sigma,TypingError te))
+let raise_type_error ?loc (env,sigma,te) =
+  Loc.raise ?loc (PretypeError(env,sigma,TypingError te))
 
-
-let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty reason =
+let error_actual_type ?loc env sigma {uj_val=c;uj_type=actty} expty reason =
   let j = {uj_val=c;uj_type=actty} in
-  raise_pretype_error
-    (loc, env, sigma, ActualTypeNotCoercible (j, expty, reason))
+  raise_pretype_error ?loc
+    (env, sigma, ActualTypeNotCoercible (j, expty, reason))
 
-let error_cant_apply_not_functional_loc loc env sigma rator randl =
-  raise_located_type_error
-    (loc, env, sigma, CantApplyNonFunctional (rator, Array.of_list randl))
+let error_cant_apply_not_functional ?loc env sigma rator randl =
+  raise_type_error ?loc
+    (env, sigma, CantApplyNonFunctional (rator, Array.of_list randl))
 
-let error_cant_apply_bad_type_loc loc env sigma (n,c,t) rator randl =
-  raise_located_type_error
-    (loc, env, sigma,
+let error_cant_apply_bad_type ?loc env sigma (n,c,t) rator randl =
+  raise_type_error ?loc
+    (env, sigma,
        CantApplyBadType ((n,c,t), rator, Array.of_list randl))
 
-let error_ill_formed_branch_loc loc env sigma c i actty expty =
-  raise_located_type_error
-    (loc, env, sigma, IllFormedBranch (c, i, actty, expty))
+let error_ill_formed_branch ?loc env sigma c i actty expty =
+  raise_type_error
+    ?loc (env, sigma, IllFormedBranch (c, i, actty, expty))
 
-let error_number_branches_loc loc env sigma cj expn =
-  raise_located_type_error (loc, env, sigma, NumberBranches (cj, expn))
+let error_number_branches ?loc env sigma cj expn =
+  raise_type_error ?loc (env, sigma, NumberBranches (cj, expn))
 
-let error_case_not_inductive_loc loc env sigma cj =
-  raise_located_type_error (loc, env, sigma, CaseNotInductive cj)
+let error_case_not_inductive ?loc env sigma cj =
+  raise_type_error ?loc (env, sigma, CaseNotInductive cj)
 
-let error_ill_typed_rec_body_loc loc env sigma i na jl tys =
-  raise_located_type_error
-    (loc, env, sigma, IllTypedRecBody (i, na, jl, tys))
+let error_ill_typed_rec_body ?loc env sigma i na jl tys =
+  raise_type_error ?loc
+    (env, sigma, IllTypedRecBody (i, na, jl, tys))
 
-let error_not_a_type_loc loc env sigma j =
-  raise_located_type_error (loc, env, sigma, NotAType j)
+let error_not_a_type ?loc env sigma j =
+  raise_type_error ?loc (env, sigma, NotAType j)
 
 (*s Implicit arguments synthesis errors. It is hard to find
     a precise location. *)
@@ -108,15 +107,12 @@ let error_not_a_type_loc loc env sigma j =
 let error_occur_check env sigma ev c =
   raise (PretypeError (env, sigma, UnifOccurCheck (ev,c)))
 
-let error_unsolvable_implicit loc env sigma evk explain =
-  Loc.raise loc
+let error_unsolvable_implicit ?loc env sigma evk explain =
+  Loc.raise ?loc
     (PretypeError (env, sigma, UnsolvableImplicit (evk, explain)))
 
-let error_cannot_unify_loc loc env sigma ?reason (m,n) =
-  Loc.raise loc (PretypeError (env, sigma,CannotUnify (m,n,reason)))
-
-let error_cannot_unify env sigma ?reason (m,n) =
-  raise (PretypeError (env, sigma,CannotUnify (m,n,reason)))
+let error_cannot_unify ?loc env sigma ?reason (m,n) =
+  Loc.raise ?loc (PretypeError (env, sigma,CannotUnify (m,n,reason)))
 
 let error_cannot_unify_local env sigma (m,n,sn) =
   raise (PretypeError (env, sigma,CannotUnifyLocal (m,n,sn)))
@@ -140,21 +136,21 @@ let error_non_linear_unification env sigma hdmeta t =
 
 (*s Ml Case errors *)
 
-let error_cant_find_case_type_loc loc env sigma expr =
-  raise_pretype_error (loc, env, sigma, CantFindCaseType expr)
+let error_cant_find_case_type ?loc env sigma expr =
+  raise_pretype_error ?loc (env, sigma, CantFindCaseType expr)
 
 (*s Pretyping errors *)
 
-let error_unexpected_type_loc loc env sigma actty expty =
-  raise_pretype_error (loc, env, sigma, UnexpectedType (actty, expty))
+let error_unexpected_type ?loc env sigma actty expty =
+  raise_pretype_error ?loc (env, sigma, UnexpectedType (actty, expty))
 
-let error_not_product_loc loc env sigma c =
-  raise_pretype_error (loc, env, sigma, NotProduct c)
+let error_not_product ?loc env sigma c =
+  raise_pretype_error ?loc (env, sigma, NotProduct c)
 
 (*s Error in conversion from AST to glob_constr *)
 
-let error_var_not_found_loc loc s =
-  raise_pretype_error (loc, empty_env, Evd.empty, VarNotFound s)
+let error_var_not_found ?loc s =
+  raise_pretype_error ?loc (empty_env, Evd.empty, VarNotFound s)
 
 (*s Typeclass errors *)
 
@@ -166,7 +162,7 @@ let unsatisfiable_constraints env evd ev comp =
   | Some ev ->
     let loc, kind = Evd.evar_source ev evd in
     let err = UnsatisfiableConstraints (Some (ev, kind), comp) in
-    Loc.raise loc (PretypeError (env,evd,err))
+    Loc.raise ~loc (PretypeError (env,evd,err))
 
 let unsatisfiable_exception exn =
   match exn with
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 880f48e5f9..73f81923ff 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -64,35 +64,35 @@ exception PretypeError of env * Evd.evar_map * pretype_error
 val precatchable_exception : exn -> bool
 
 (** Raising errors *)
-val error_actual_type_loc :
-  Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr ->
+val error_actual_type :
+  ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr ->
       unification_error -> 'b
 
-val error_cant_apply_not_functional_loc :
-  Loc.t -> env -> Evd.evar_map ->
+val error_cant_apply_not_functional :
+  ?loc:Loc.t -> env -> Evd.evar_map ->
       unsafe_judgment -> unsafe_judgment list -> 'b
 
-val error_cant_apply_bad_type_loc :
-  Loc.t -> env -> Evd.evar_map -> int * constr * constr ->
+val error_cant_apply_bad_type :
+  ?loc:Loc.t -> env -> Evd.evar_map -> int * constr * constr ->
       unsafe_judgment -> unsafe_judgment list -> 'b
 
-val error_case_not_inductive_loc :
-  Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
+val error_case_not_inductive :
+  ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
 
-val error_ill_formed_branch_loc :
-  Loc.t -> env -> Evd.evar_map ->
+val error_ill_formed_branch :
+  ?loc:Loc.t -> env -> Evd.evar_map ->
       constr -> pconstructor -> constr -> constr -> 'b
 
-val error_number_branches_loc :
-  Loc.t -> env -> Evd.evar_map ->
+val error_number_branches :
+  ?loc:Loc.t -> env -> Evd.evar_map ->
       unsafe_judgment -> int -> 'b
 
-val error_ill_typed_rec_body_loc :
-  Loc.t -> env -> Evd.evar_map ->
+val error_ill_typed_rec_body :
+  ?loc:Loc.t -> env -> Evd.evar_map ->
       int -> Name.t array -> unsafe_judgment array -> types array -> 'b
 
-val error_not_a_type_loc :
-  Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
+val error_not_a_type :
+  ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
 
 val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
 
@@ -101,15 +101,12 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
 val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b
 
 val error_unsolvable_implicit :
-  Loc.t -> env -> Evd.evar_map -> existential_key ->
+  ?loc:Loc.t -> env -> Evd.evar_map -> existential_key ->
       Evd.unsolvability_explanation option -> 'b
 
-val error_cannot_unify_loc : Loc.t -> env -> Evd.evar_map ->
+val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map ->
   ?reason:unification_error -> constr * constr -> 'b
 
-val error_cannot_unify : env -> Evd.evar_map -> ?reason:unification_error ->
-  constr * constr -> 'b
-
 val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b
 
 val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map ->
@@ -126,20 +123,20 @@ val error_non_linear_unification : env -> Evd.evar_map ->
 
 (** {6 Ml Case errors } *)
 
-val error_cant_find_case_type_loc :
-  Loc.t -> env -> Evd.evar_map -> constr -> 'b
+val error_cant_find_case_type :
+  ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b
 
 (** {6 Pretyping errors } *)
 
-val error_unexpected_type_loc :
-  Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b
+val error_unexpected_type :
+  ?loc:Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b
 
-val error_not_product_loc :
-  Loc.t -> env -> Evd.evar_map -> constr -> 'b
+val error_not_product :
+  ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b
 
 (** {6 Error in conversion from AST to glob_constr } *)
 
-val error_var_not_found_loc : Loc.t -> Id.t -> 'b
+val error_var_not_found : ?loc:Loc.t -> Id.t -> 'b
 
 (** {6 Typeclass errors } *)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1ef96e0344..8b0bdb0092 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -160,7 +160,7 @@ let search_guard loc env possible_indexes fixdefs =
 	    with TypeError _ -> ())
 	 (List.combinations possible_indexes);
        let errmsg = "Cannot guess decreasing argument of fix." in
-	 user_err_loc (loc,"search_guard", Pp.str errmsg)
+	 user_err ~loc "search_guard" (Pp.str errmsg)
      with Found indexes -> indexes)
 
 (* To force universe name declaration before use *)
@@ -211,8 +211,8 @@ let interp_universe_level_name evd (loc,s) =
 	with Not_found -> 
 	  if not (is_strict_universe_declarations ()) then
   	    new_univ_level_variable ~loc ~name:s univ_rigid evd
-	  else user_err_loc (loc, "interp_universe_level_name",
-			     Pp.(str "Undeclared universe: " ++ str s))
+	  else user_err ~loc "interp_universe_level_name"
+			     (Pp.(str "Undeclared universe: " ++ str s))
 
 let interp_universe ?loc evd = function
   | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in
@@ -298,7 +298,7 @@ let check_extra_evars_are_solved env current_sigma pending =
 	match k with
 	| Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
 	| _ ->
-	    error_unsolvable_implicit loc env current_sigma evk None) pending
+	    error_unsolvable_implicit ~loc env current_sigma evk None) pending
 
 (* [check_evars] fails if some unresolved evar remains *)
 
@@ -313,7 +313,7 @@ let check_evars env initial_sigma sigma c =
             let (loc,k) = evar_source evk sigma in
 	      match k with
 	      | Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
-	      | _ -> Pretype_errors.error_unsolvable_implicit loc env sigma evk None)
+	      | _ -> Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None)
       | _ -> Constr.iter proc_rec c
   in proc_rec c
 
@@ -359,7 +359,7 @@ let evar_type_fixpoint loc env evdref lna lar vdefj =
       for i = 0 to lt-1 do
         if not (e_cumul env.ExtraEnv.env evdref (vdefj.(i)).uj_type
 		  (lift lt lar.(i))) then
-          error_ill_typed_rec_body_loc loc env.ExtraEnv.env !evdref
+          error_ill_typed_rec_body ~loc env.ExtraEnv.env !evdref
             i lna vdefj lar
       done
 
@@ -373,9 +373,9 @@ let check_instance loc subst = function
   | [] -> ()
   | (id,_) :: _ ->
       if List.mem_assoc id subst then
-        user_err_loc (loc,"",pr_id id ++ str "appears more than once.")
+        user_err ~loc "" (pr_id id ++ str "appears more than once.")
       else
-        user_err_loc (loc,"",str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".")
+        user_err ~loc "" (str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".")
 
 (* used to enforce a name in Lambda when the type constraints itself
    is named, hence possibly dependent *)
@@ -454,8 +454,8 @@ let pretype_id pretype k0 loc env evdref lvar id =
 	(* and build a nice error message *)
       if Id.Map.mem id lvar.ltac_genargs then begin
         let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in
-	user_err_loc (loc,"",
-          str "Variable " ++ pr_id id ++ str " should be bound to a term but is \
+	user_err ~loc ""
+         (str "Variable " ++ pr_id id ++ str " should be bound to a term but is \
           bound to a " ++ Geninterp.Val.pr typ ++ str ".")
       end;
       (* Check if [id] is a section or goal variable *)
@@ -463,7 +463,7 @@ let pretype_id pretype k0 loc env evdref lvar id =
 	  { uj_val  = mkVar id; uj_type = (get_type (lookup_named id env)) }
       with Not_found ->
 	  (* [id] not found, standard error message *)
-	  error_var_not_found_loc loc id
+	  error_var_not_found ~loc id
 
 let evar_kind_of_term sigma c =
   kind_of_term (whd_evar sigma c)
@@ -486,16 +486,16 @@ let pretype_global loc rigid env evd gr us =
        let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in
        let len = Array.length arr in
        if len != List.length l then
-	 user_err_loc (loc, "pretype", 
-		       str "Universe instance should have length " ++ int len)
+	 user_err ~loc "pretype"
+		       (str "Universe instance should have length " ++ int len)
        else
 	 let evd, l' = List.fold_left (fun (evd, univs) l -> 
 	    let evd, l = interp_universe_level_name loc evd l in
 	      (evd, l :: univs)) (evd, []) l
 	 in
 	 if List.exists (fun l -> Univ.Level.is_prop l) l' then
-	   user_err_loc (loc, "pretype",
-		 str "Universe instances cannot contain Prop, polymorphic" ++
+	   user_err ~loc "pretype"
+		 (str "Universe instances cannot contain Prop, polymorphic" ++
 		   str " universe instances must be greater or equal to Set.");
 	 evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
   in
@@ -510,7 +510,7 @@ let pretype_ref loc evdref env ref us =
          (* This may happen if env is a goal env and section variables have
             been cleared - section variables should be different from goal
             variables *)
-         Pretype_errors.error_var_not_found_loc loc id)
+         Pretype_errors.error_var_not_found ~loc id)
   | ref ->
     let evd, c = pretype_global loc univ_flexible env !evdref ref us in
     let () = evdref := evd in
@@ -566,7 +566,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       let evk =
         try Evd.evar_key id !evdref
         with Not_found ->
-          user_err_loc (loc,"",str "Unknown existential variable.") in
+          user_err ~loc "" (str "Unknown existential variable.") in
       let hyps = evar_filtered_context (Evd.find !evdref evk) in
       let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in
       let c = mkEvar (evk, args) in
@@ -749,9 +749,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 		
 	  | _ ->
 	    let hj = pretype empty_tycon env evdref lvar c in
-	      error_cant_apply_not_functional_loc
-		(Loc.merge floc argloc) env.ExtraEnv.env !evdref
-	      	resj [hj]
+	      error_cant_apply_not_functional
+                ~loc:(Loc.merge floc argloc) env.ExtraEnv.env !evdref
+                resj [hj]
     in
     let resj = apply_rec env 1 fj candargs args in
     let resj =
@@ -844,15 +844,15 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       try find_rectype env.ExtraEnv.env !evdref cj.uj_type
       with Not_found ->
 	let cloc = loc_of_glob_constr c in
-	  error_case_not_inductive_loc cloc env.ExtraEnv.env !evdref cj
+	  error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj
     in
     let cstrs = get_constructors env.ExtraEnv.env indf in
     if not (Int.equal (Array.length cstrs) 1) then
-      user_err_loc (loc,"",str "Destructing let is only for inductive types" ++
+      user_err ~loc "" (str "Destructing let is only for inductive types" ++
 	str " with one constructor.");
     let cs = cstrs.(0) in
     if not (Int.equal (List.length nal) cs.cs_nargs) then
-      user_err_loc (loc,"", str "Destructing let on this type expects " ++ 
+      user_err ~loc:loc "" (str "Destructing let on this type expects " ++ 
 	int cs.cs_nargs ++ str " variables.");
     let fsign, record = 
       match get_projections env.ExtraEnv.env indf with
@@ -918,7 +918,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	      if noccur_between 1 cs.cs_nargs ccl then
 		lift (- cs.cs_nargs) ccl
 	      else
-		error_cant_find_case_type_loc loc env.ExtraEnv.env !evdref
+		error_cant_find_case_type ~loc env.ExtraEnv.env !evdref
 		  cj.uj_val in
 		 (* let ccl = refresh_universes ccl in *)
 	    let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
@@ -934,11 +934,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       try find_rectype env.ExtraEnv.env !evdref cj.uj_type
       with Not_found ->
 	let cloc = loc_of_glob_constr c in
-	  error_case_not_inductive_loc cloc env.ExtraEnv.env !evdref cj in
+	  error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj in
     let cstrs = get_constructors env.ExtraEnv.env indf in
       if not (Int.equal (Array.length cstrs) 2) then
-        user_err_loc (loc,"",
-		      str "If is only for inductive types with two constructors.");
+        user_err ~loc ""
+		      (str "If is only for inductive types with two constructors.");
 
       let arsgn =
 	let arsgn,_ = get_arity env.ExtraEnv.env indf in
@@ -1020,9 +1020,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 		let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in
 		if b then (evdref := evd; cj, tval)
 		else
-		  error_actual_type_loc loc env.ExtraEnv.env !evdref cj tval 
+		  error_actual_type ~loc env.ExtraEnv.env !evdref cj tval 
                       (ConversionFailed (env.ExtraEnv.env,cty,tval))
-	      else user_err_loc (loc,"",str "Cannot check cast with vm: " ++
+	      else user_err ~loc "" (str "Cannot check cast with vm: " ++
 		str "unresolved arguments remain.")
 	  | NATIVEcast ->
  	    let cj = pretype empty_tycon env evdref lvar c in
@@ -1031,7 +1031,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	      let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in
 	      if b then (evdref := evd; cj, tval)
 	      else
-                error_actual_type_loc loc env.ExtraEnv.env !evdref cj tval 
+                error_actual_type ~loc env.ExtraEnv.env !evdref cj tval
                   (ConversionFailed (env.ExtraEnv.env,cty,tval))
             end
 	  | _ -> 
@@ -1059,7 +1059,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
         let t' = lookup_named id env |> get_type in
         if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found
       with Not_found ->
-        user_err_loc (loc,"",str "Cannot interpret " ++
+        user_err ~loc "" (str "Cannot interpret " ++
           pr_existential_key !evdref evk ++
           str " in current context: no binding for " ++ pr_id id ++ str ".") in
     ((id,c)::subst, update) in
@@ -1097,8 +1097,8 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
 	| Some v ->
 	    if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj
 	    else
-	      error_unexpected_type_loc
-                (loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v
+	      error_unexpected_type
+                ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v
 
 let ise_pretype_gen flags env sigma lvar kind c =
   let env = make_env env in
-- 
cgit v1.2.3


From 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Aug 2016 01:58:04 +0200
Subject: Remove errorlabstrm in favor of user_err

As noted by @ppedrot, the first is redundant. The patch is basically a renaming.

We didn't make the component optional yet, but this could happen in a
future patch.
---
 pretyping/cases.ml        |  2 +-
 pretyping/classops.ml     |  2 +-
 pretyping/find_subterm.ml |  2 +-
 pretyping/indrec.ml       |  4 ++--
 pretyping/inductiveops.ml |  2 +-
 pretyping/patternops.ml   |  2 +-
 pretyping/pretyping.ml    |  6 +++---
 pretyping/recordops.ml    |  2 +-
 pretyping/tacred.ml       | 14 +++++++-------
 pretyping/unification.ml  |  4 ++--
 10 files changed, 20 insertions(+), 20 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 85c518019e..18ad2ed3d0 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -503,7 +503,7 @@ let set_used_pattern eqn = eqn.used := true
 
 let extract_rhs pb =
   match pb.mat with
-    | [] -> errorlabstrm "build_leaf" (msg_may_need_inversion())
+    | [] -> user_err "build_leaf" (msg_may_need_inversion())
     | eqn::_ ->
 	set_used_pattern eqn;
         eqn.rhs
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 4f265e76c9..92a0ca9887 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -538,7 +538,7 @@ let inheritance_graph () =
 let coercion_of_reference r =
   let ref = Nametab.global r in
   if not (coercion_exists ref) then
-    errorlabstrm "try_add_coercion"
+    user_err "try_add_coercion"
       (Nametab.pr_global_env Id.Set.empty ref ++ str" is not a coercion.");
   ref
 
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 4caa1e9927..c7909a3c7b 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -35,7 +35,7 @@ let explain_occurrence_error = function
   | IncorrectInValueOccurrence id -> explain_incorrect_in_value_occurrence id
 
 let error_occurrences_error e =
-  errorlabstrm "" (explain_occurrence_error e)
+  user_err "" (explain_occurrence_error e)
 
 let error_invalid_occurrence occ =
   error_occurrences_error (InvalidOccurrence occ)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 39aeb41f77..0061d8ae95 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -55,7 +55,7 @@ let is_private mib =
 
 let check_privacy_block mib =
   if is_private mib then
-    errorlabstrm ""(str"case analysis on a private inductive type")
+    user_err ""(str"case analysis on a private inductive type")
       
 (**********************************************************************)
 (* Building case analysis schemes *)
@@ -594,7 +594,7 @@ let lookup_eliminator ind_sp s =
   (* using short name (e.g. for "eq_rec") *)
   try Nametab.locate (qualid_of_ident id)
   with Not_found ->
-    errorlabstrm "default_elim"
+    user_err "default_elim"
       (strbrk "Cannot find the elimination combinator " ++
        pr_id id ++ strbrk ", the elimination of the inductive definition " ++
        pr_global_env Id.Set.empty (IndRef ind_sp) ++
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 214e19fecf..cb69ab36f2 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -355,7 +355,7 @@ let make_case_or_project env indf ci pred c branches =
        let mib, _ = Inductive.lookup_mind_specif env ind in
        if (* dependent *) not (noccurn 1 t) &&
           not (has_dependent_elim mib) then
-       errorlabstrm "make_case_or_project"
+       user_err "make_case_or_project"
 		    Pp.(str"Dependent case analysis not allowed" ++
 		     str" on inductive type " ++ Names.MutInd.print (fst ind))
      in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 99c3772db9..aa795106a8 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -204,7 +204,7 @@ let error_instantiate_pattern id l =
   | [_] -> "is" 
   | _ -> "are"
   in
-  errorlabstrm "" (str "Cannot substitute the term bound to " ++ pr_id id
+  user_err "" (str "Cannot substitute the term bound to " ++ pr_id id
     ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l
     ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8b0bdb0092..cdb39207e5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -390,7 +390,7 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function
       try Name (Id.Map.find id ltac_idents)
       with Not_found ->
         if Id.Map.mem id ltac_genargs then
-          errorlabstrm "" (str"Ltac variable"++spc()++ pr_id id ++
+          user_err "" (str"Ltac variable"++spc()++ pr_id id ++
                            spc()++str"is not bound to an identifier."++spc()++
                            str"It cannot be used in a binder.")
         else n
@@ -411,14 +411,14 @@ let invert_ltac_bound_name lvar env id0 id =
   let id' = Id.Map.find id lvar.ltac_idents in
   try mkRel (pi1 (lookup_rel_id id' (rel_context env)))
   with Not_found ->
-    errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
+    user_err "" (str "Ltac variable " ++ pr_id id0 ++
 		       str " depends on pattern variable name " ++ pr_id id ++
 		       str " which is not bound in current context.")
 
 let protected_get_type_of env sigma c =
   try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c
   with Retyping.RetypeError _ ->
-    errorlabstrm ""
+    user_err ""
       (str "Cannot reinterpret " ++ quote (print_constr c) ++
        str " in the current environment.")
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 284af0cb15..945ef5daac 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -291,7 +291,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
 (*s High-level declaration of a canonical structure *)
 
 let error_not_structure ref =
-  errorlabstrm "object_declare"
+  user_err "object_declare"
     (Nameops.pr_id (basename_of_global ref) ++ str" is not a structure object.")
 
 let check_and_decompose_canonical_structure ref =
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 820a81b5d2..67819dc986 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -38,7 +38,7 @@ exception Elimconst
 exception Redelimination
 
 let error_not_evaluable r =
-  errorlabstrm "error_not_evaluable"
+  user_err "error_not_evaluable"
     (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++
      spc () ++ str "to an evaluable reference.")
 
@@ -993,7 +993,7 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
       incr pos;
       if ok then begin
         if Option.has_some nested then
-          errorlabstrm "" (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str ".");
+          user_err "" (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str ".");
         (* Skip inner occurrences for stable counting of occurrences *)
         if locs != [] then
           ignore (traverse_below (Some (!pos-1)) envc t);
@@ -1159,13 +1159,13 @@ let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
 let check_privacy env ind =
   let spec = Inductive.lookup_mind_specif env (fst ind) in
   if Inductive.is_private spec then
-    errorlabstrm "" (str "case analysis on a private type.")
+    user_err "" (str "case analysis on a private type.")
   else ind
 
 let check_not_primitive_record env ind =
   let spec = Inductive.lookup_mind_specif env (fst ind) in
     if Inductive.is_primitive_record spec then
-      errorlabstrm "" (str "case analysis on a primitive record type: " ++
+      user_err "" (str "case analysis on a primitive record type: " ++
 		       str "use projections or let instead.")
     else ind
 
@@ -1182,14 +1182,14 @@ let reduce_to_ind_gen allow_product env sigma t =
 	  if allow_product then
 	    elimrec (push_rel (LocalAssum (n,ty)) env) t' ((LocalAssum (n,ty))::l)
 	  else
-	    errorlabstrm "" (str"Not an inductive definition.")
+	    user_err "" (str"Not an inductive definition.")
       | _ ->
 	  (* Last chance: we allow to bypass the Opaque flag (as it
 	     was partially the case between V5.10 and V8.1 *)
 	  let t' = whd_all env sigma t in
 	  match kind_of_term (fst (decompose_app t')) with
 	    | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l)
-	    | _ -> errorlabstrm "" (str"Not an inductive product.")
+	    | _ -> user_err "" (str"Not an inductive product.")
   in
   elimrec env t []
 
@@ -1239,7 +1239,7 @@ let one_step_reduce env sigma c =
   applist (redrec (c,[]))
 
 let error_cannot_recognize ref =
-  errorlabstrm ""
+  user_err ""
     (str "Cannot recognize a statement based on " ++
      Nametab.pr_global_env Id.Set.empty ref ++ str".")
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0c1ce0d2f8..5e3c3c2598 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1586,7 +1586,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     let ids = ids_of_named_context (named_context env) in
     if name == Anonymous then next_ident_away_in_goal x ids else
     if mem_named_context x (named_context env) then
-      errorlabstrm "Unification.make_abstraction_core"
+      user_err "Unification.make_abstraction_core"
         (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.")
     else
       x
@@ -1600,7 +1600,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
         if indirectly_dependent c d depdecls then
           (* Told explicitly not to abstract over [d], but it is dependent *)
           let id' = indirect_dependency d depdecls in
-          errorlabstrm "" (str "Cannot abstract over " ++ Nameops.pr_id id'
+          user_err "" (str "Cannot abstract over " ++ Nameops.pr_id id'
             ++ str " without also abstracting or erasing " ++ Nameops.pr_id hyp
             ++ str ".")
         else
-- 
cgit v1.2.3


From fc579fdc83b751a44a18d2373e86ab38806e7306 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Aug 2016 02:35:47 +0200
Subject: Make the user_err header an optional parameter.

Suggested by @ppedrot
---
 pretyping/cases.ml        |  6 +++---
 pretyping/classops.ml     |  2 +-
 pretyping/detyping.ml     |  4 ++--
 pretyping/find_subterm.ml |  2 +-
 pretyping/indrec.ml       |  4 ++--
 pretyping/inductiveops.ml |  2 +-
 pretyping/patternops.ml   |  6 +++---
 pretyping/pretyping.ml    | 32 ++++++++++++++++----------------
 pretyping/recordops.ml    |  2 +-
 pretyping/reductionops.ml |  2 +-
 pretyping/tacred.ml       | 14 +++++++-------
 pretyping/unification.ml  |  4 ++--
 12 files changed, 40 insertions(+), 40 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 18ad2ed3d0..0e659aec93 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -503,7 +503,7 @@ let set_used_pattern eqn = eqn.used := true
 
 let extract_rhs pb =
   match pb.mat with
-    | [] -> user_err "build_leaf" (msg_may_need_inversion())
+    | [] -> user_err ~hdr:"build_leaf" (msg_may_need_inversion())
     | eqn::_ ->
 	set_used_pattern eqn;
         eqn.rhs
@@ -1832,7 +1832,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 		       | None -> [LocalAssum (na, lift n typ)]
 		       | Some b -> [LocalDef (na, lift n b, lift n typ)])
 	    | Some (loc,_,_) ->
- 	    user_err ~loc ""
+ 	    user_err ~loc 
                 (str"Unexpected type annotation for a term of non inductive type."))
       | IsInd (term,IndType(indf,realargs),_) ->
           let indf' = if dolift then lift_inductive_family n indf else indf in
@@ -1843,7 +1843,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 	    match t with
 	      | Some (loc,ind',realnal) ->
 		  if not (eq_ind ind ind') then
-		    user_err ~loc "" (str "Wrong inductive type.");
+		    user_err ~loc  (str "Wrong inductive type.");
 		  if not (Int.equal nrealargs_ctxt (List.length realnal)) then
 		      anomaly (Pp.str "Ill-formed 'in' clause in cases");
 		  List.rev realnal
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 92a0ca9887..30d100af9f 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -538,7 +538,7 @@ let inheritance_graph () =
 let coercion_of_reference r =
   let ref = Nametab.global r in
   if not (coercion_exists ref) then
-    user_err "try_add_coercion"
+    user_err ~hdr:"try_add_coercion"
       (Nametab.pr_global_env Id.Set.empty ref ++ str" is not a coercion.");
   ref
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index ab93939150..cad5551c15 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -67,14 +67,14 @@ let isomorphic_to_tuple lc = Int.equal (Array.length lc) 1
 let encode_bool r =
   let (x,lc) = encode_inductive r in
   if not (has_two_constructors lc) then
-    user_err ~loc:(loc_of_reference r) "encode_if"
+    user_err ~loc:(loc_of_reference r) ~hdr:"encode_if"
       (str "This type has not exactly two constructors.");
   x
 
 let encode_tuple r =
   let (x,lc) = encode_inductive r in
   if not (isomorphic_to_tuple lc) then
-    user_err ~loc:(loc_of_reference r) "encode_tuple"
+    user_err ~loc:(loc_of_reference r) ~hdr:"encode_tuple"
       (str "This type cannot be seen as a tuple type.");
   x
 
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index c7909a3c7b..38b6075e5a 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -35,7 +35,7 @@ let explain_occurrence_error = function
   | IncorrectInValueOccurrence id -> explain_incorrect_in_value_occurrence id
 
 let error_occurrences_error e =
-  user_err "" (explain_occurrence_error e)
+  user_err  (explain_occurrence_error e)
 
 let error_invalid_occurrence occ =
   error_occurrences_error (InvalidOccurrence occ)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 0061d8ae95..9cf91a9476 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -55,7 +55,7 @@ let is_private mib =
 
 let check_privacy_block mib =
   if is_private mib then
-    user_err ""(str"case analysis on a private inductive type")
+    user_err (str"case analysis on a private inductive type")
       
 (**********************************************************************)
 (* Building case analysis schemes *)
@@ -594,7 +594,7 @@ let lookup_eliminator ind_sp s =
   (* using short name (e.g. for "eq_rec") *)
   try Nametab.locate (qualid_of_ident id)
   with Not_found ->
-    user_err "default_elim"
+    user_err ~hdr:"default_elim"
       (strbrk "Cannot find the elimination combinator " ++
        pr_id id ++ strbrk ", the elimination of the inductive definition " ++
        pr_global_env Id.Set.empty (IndRef ind_sp) ++
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index cb69ab36f2..29f57144a9 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -355,7 +355,7 @@ let make_case_or_project env indf ci pred c branches =
        let mib, _ = Inductive.lookup_mind_specif env ind in
        if (* dependent *) not (noccurn 1 t) &&
           not (has_dependent_elim mib) then
-       user_err "make_case_or_project"
+       user_err ~hdr:"make_case_or_project"
 		    Pp.(str"Dependent case analysis not allowed" ++
 		     str" on inductive type " ++ Names.MutInd.print (fst ind))
      in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index aa795106a8..9dcb5d2a57 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -204,7 +204,7 @@ let error_instantiate_pattern id l =
   | [_] -> "is" 
   | _ -> "are"
   in
-  user_err "" (str "Cannot substitute the term bound to " ++ pr_id id
+  user_err  (str "Cannot substitute the term bound to " ++ pr_id id
     ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l
     ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")
 
@@ -315,7 +315,7 @@ let rec subst_pattern subst pat =
 let mkPLambda na b = PLambda(na,PMeta None,b)
 let rev_it_mkPLambda = List.fold_right mkPLambda
 
-let err ?loc pp = user_err ?loc "pattern_of_glob_constr" pp
+let err ?loc pp = user_err ?loc ~hdr:"pattern_of_glob_constr" pp
 
 let warn_cast_in_pattern =
   CWarnings.create ~name:"cast-in-pattern" ~category:"automation"
@@ -387,7 +387,7 @@ let rec pat_of_raw metas vars = function
           rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
         | (None | Some (GHole _)), _ -> PMeta None
 	| Some p, None ->
-            user_err ~loc "" (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
+            user_err ~loc  (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
       in
       let info =
 	{ cip_style = sty;
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index cdb39207e5..3e65363d68 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -160,7 +160,7 @@ let search_guard loc env possible_indexes fixdefs =
 	    with TypeError _ -> ())
 	 (List.combinations possible_indexes);
        let errmsg = "Cannot guess decreasing argument of fix." in
-	 user_err ~loc "search_guard" (Pp.str errmsg)
+	 user_err ~loc ~hdr:"search_guard" (Pp.str errmsg)
      with Found indexes -> indexes)
 
 (* To force universe name declaration before use *)
@@ -211,7 +211,7 @@ let interp_universe_level_name evd (loc,s) =
 	with Not_found -> 
 	  if not (is_strict_universe_declarations ()) then
   	    new_univ_level_variable ~loc ~name:s univ_rigid evd
-	  else user_err ~loc "interp_universe_level_name"
+	  else user_err ~loc ~hdr:"interp_universe_level_name"
 			     (Pp.(str "Undeclared universe: " ++ str s))
 
 let interp_universe ?loc evd = function
@@ -373,9 +373,9 @@ let check_instance loc subst = function
   | [] -> ()
   | (id,_) :: _ ->
       if List.mem_assoc id subst then
-        user_err ~loc "" (pr_id id ++ str "appears more than once.")
+        user_err ~loc  (pr_id id ++ str "appears more than once.")
       else
-        user_err ~loc "" (str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".")
+        user_err ~loc  (str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".")
 
 (* used to enforce a name in Lambda when the type constraints itself
    is named, hence possibly dependent *)
@@ -390,7 +390,7 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function
       try Name (Id.Map.find id ltac_idents)
       with Not_found ->
         if Id.Map.mem id ltac_genargs then
-          user_err "" (str"Ltac variable"++spc()++ pr_id id ++
+          user_err  (str"Ltac variable"++spc()++ pr_id id ++
                            spc()++str"is not bound to an identifier."++spc()++
                            str"It cannot be used in a binder.")
         else n
@@ -411,14 +411,14 @@ let invert_ltac_bound_name lvar env id0 id =
   let id' = Id.Map.find id lvar.ltac_idents in
   try mkRel (pi1 (lookup_rel_id id' (rel_context env)))
   with Not_found ->
-    user_err "" (str "Ltac variable " ++ pr_id id0 ++
+    user_err  (str "Ltac variable " ++ pr_id id0 ++
 		       str " depends on pattern variable name " ++ pr_id id ++
 		       str " which is not bound in current context.")
 
 let protected_get_type_of env sigma c =
   try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c
   with Retyping.RetypeError _ ->
-    user_err ""
+    user_err 
       (str "Cannot reinterpret " ++ quote (print_constr c) ++
        str " in the current environment.")
 
@@ -454,7 +454,7 @@ let pretype_id pretype k0 loc env evdref lvar id =
 	(* and build a nice error message *)
       if Id.Map.mem id lvar.ltac_genargs then begin
         let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in
-	user_err ~loc ""
+	user_err ~loc 
          (str "Variable " ++ pr_id id ++ str " should be bound to a term but is \
           bound to a " ++ Geninterp.Val.pr typ ++ str ".")
       end;
@@ -486,7 +486,7 @@ let pretype_global loc rigid env evd gr us =
        let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in
        let len = Array.length arr in
        if len != List.length l then
-	 user_err ~loc "pretype"
+	 user_err ~loc ~hdr:"pretype"
 		       (str "Universe instance should have length " ++ int len)
        else
 	 let evd, l' = List.fold_left (fun (evd, univs) l -> 
@@ -494,7 +494,7 @@ let pretype_global loc rigid env evd gr us =
 	      (evd, l :: univs)) (evd, []) l
 	 in
 	 if List.exists (fun l -> Univ.Level.is_prop l) l' then
-	   user_err ~loc "pretype"
+	   user_err ~loc ~hdr:"pretype"
 		 (str "Universe instances cannot contain Prop, polymorphic" ++
 		   str " universe instances must be greater or equal to Set.");
 	 evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
@@ -566,7 +566,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       let evk =
         try Evd.evar_key id !evdref
         with Not_found ->
-          user_err ~loc "" (str "Unknown existential variable.") in
+          user_err ~loc  (str "Unknown existential variable.") in
       let hyps = evar_filtered_context (Evd.find !evdref evk) in
       let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in
       let c = mkEvar (evk, args) in
@@ -848,11 +848,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     in
     let cstrs = get_constructors env.ExtraEnv.env indf in
     if not (Int.equal (Array.length cstrs) 1) then
-      user_err ~loc "" (str "Destructing let is only for inductive types" ++
+      user_err ~loc  (str "Destructing let is only for inductive types" ++
 	str " with one constructor.");
     let cs = cstrs.(0) in
     if not (Int.equal (List.length nal) cs.cs_nargs) then
-      user_err ~loc:loc "" (str "Destructing let on this type expects " ++ 
+      user_err ~loc:loc (str "Destructing let on this type expects " ++ 
 	int cs.cs_nargs ++ str " variables.");
     let fsign, record = 
       match get_projections env.ExtraEnv.env indf with
@@ -937,7 +937,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj in
     let cstrs = get_constructors env.ExtraEnv.env indf in
       if not (Int.equal (Array.length cstrs) 2) then
-        user_err ~loc ""
+        user_err ~loc 
 		      (str "If is only for inductive types with two constructors.");
 
       let arsgn =
@@ -1022,7 +1022,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 		else
 		  error_actual_type ~loc env.ExtraEnv.env !evdref cj tval 
                       (ConversionFailed (env.ExtraEnv.env,cty,tval))
-	      else user_err ~loc "" (str "Cannot check cast with vm: " ++
+	      else user_err ~loc  (str "Cannot check cast with vm: " ++
 		str "unresolved arguments remain.")
 	  | NATIVEcast ->
  	    let cj = pretype empty_tycon env evdref lvar c in
@@ -1059,7 +1059,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
         let t' = lookup_named id env |> get_type in
         if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found
       with Not_found ->
-        user_err ~loc "" (str "Cannot interpret " ++
+        user_err ~loc  (str "Cannot interpret " ++
           pr_existential_key !evdref evk ++
           str " in current context: no binding for " ++ pr_id id ++ str ".") in
     ((id,c)::subst, update) in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 945ef5daac..cda052b796 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -291,7 +291,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
 (*s High-level declaration of a canonical structure *)
 
 let error_not_structure ref =
-  user_err "object_declare"
+  user_err ~hdr:"object_declare"
     (Nameops.pr_id (basename_of_global ref) ++ str" is not a structure object.")
 
 let check_and_decompose_canonical_structure ref =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 5484e70b61..ba1b4a10a7 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1205,7 +1205,7 @@ let pb_equal = function
   | Reduction.CONV -> Reduction.CONV
 
 let report_anomaly _ =
-  let e = UserError ("", Pp.str "Conversion test raised an anomaly") in
+  let e = UserError (None, Pp.str "Conversion test raised an anomaly") in
   let e = CErrors.push e in
   iraise e
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 67819dc986..bb883b29f1 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -38,7 +38,7 @@ exception Elimconst
 exception Redelimination
 
 let error_not_evaluable r =
-  user_err "error_not_evaluable"
+  user_err ~hdr:"error_not_evaluable"
     (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++
      spc () ++ str "to an evaluable reference.")
 
@@ -993,7 +993,7 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
       incr pos;
       if ok then begin
         if Option.has_some nested then
-          user_err "" (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str ".");
+          user_err  (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str ".");
         (* Skip inner occurrences for stable counting of occurrences *)
         if locs != [] then
           ignore (traverse_below (Some (!pos-1)) envc t);
@@ -1159,13 +1159,13 @@ let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
 let check_privacy env ind =
   let spec = Inductive.lookup_mind_specif env (fst ind) in
   if Inductive.is_private spec then
-    user_err "" (str "case analysis on a private type.")
+    user_err  (str "case analysis on a private type.")
   else ind
 
 let check_not_primitive_record env ind =
   let spec = Inductive.lookup_mind_specif env (fst ind) in
     if Inductive.is_primitive_record spec then
-      user_err "" (str "case analysis on a primitive record type: " ++
+      user_err  (str "case analysis on a primitive record type: " ++
 		       str "use projections or let instead.")
     else ind
 
@@ -1182,14 +1182,14 @@ let reduce_to_ind_gen allow_product env sigma t =
 	  if allow_product then
 	    elimrec (push_rel (LocalAssum (n,ty)) env) t' ((LocalAssum (n,ty))::l)
 	  else
-	    user_err "" (str"Not an inductive definition.")
+	    user_err  (str"Not an inductive definition.")
       | _ ->
 	  (* Last chance: we allow to bypass the Opaque flag (as it
 	     was partially the case between V5.10 and V8.1 *)
 	  let t' = whd_all env sigma t in
 	  match kind_of_term (fst (decompose_app t')) with
 	    | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l)
-	    | _ -> user_err "" (str"Not an inductive product.")
+	    | _ -> user_err  (str"Not an inductive product.")
   in
   elimrec env t []
 
@@ -1239,7 +1239,7 @@ let one_step_reduce env sigma c =
   applist (redrec (c,[]))
 
 let error_cannot_recognize ref =
-  user_err ""
+  user_err 
     (str "Cannot recognize a statement based on " ++
      Nametab.pr_global_env Id.Set.empty ref ++ str".")
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5e3c3c2598..bc009e50a2 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1586,7 +1586,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     let ids = ids_of_named_context (named_context env) in
     if name == Anonymous then next_ident_away_in_goal x ids else
     if mem_named_context x (named_context env) then
-      user_err "Unification.make_abstraction_core"
+      user_err ~hdr:"Unification.make_abstraction_core"
         (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.")
     else
       x
@@ -1600,7 +1600,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
         if indirectly_dependent c d depdecls then
           (* Told explicitly not to abstract over [d], but it is dependent *)
           let id' = indirect_dependency d depdecls in
-          user_err "" (str "Cannot abstract over " ++ Nameops.pr_id id'
+          user_err  (str "Cannot abstract over " ++ Nameops.pr_id id'
             ++ str " without also abstracting or erasing " ++ Nameops.pr_id hyp
             ++ str ".")
         else
-- 
cgit v1.2.3