diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-07-07 04:56:24 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-08-19 01:48:30 +0200 |
| commit | de038270f72214b169d056642eb7144a79e6f126 (patch) | |
| tree | c1a5dc835f5042c79418fdbadc7b266a473b8c82 | |
| parent | 13fb26d615cdb03a4c4841c20b108deab2de60b3 (diff) | |
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.
64 files changed, 424 insertions, 429 deletions
diff --git a/checker/modops.ml b/checker/modops.ml index b720fb621..de1db6e35 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -33,7 +33,7 @@ let error_no_such_label_sub l l1 = Label.to_string l^" is missing in "^l1^".") let error_not_a_module_loc loc s = - user_err_loc (loc,"",str ("\""^Label.to_string s^"\" is not a module")) + user_err ~loc "" (str ("\""^Label.to_string s^"\" is not a module")) let error_not_a_module s = error_not_a_module_loc Loc.ghost s diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index fcee79e07..ac874befd 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,4 +1,14 @@ ========================================= += CHANGES BETWEEN COQ V8.6 AND COQ V8.7 = +========================================= + +** Error handling ** + +All error functions now take an optional parameter `?loc:Loc.t`. For +functions that used to carry a suffix `_loc`, such suffix has been +dropped. + +========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= diff --git a/engine/evd.ml b/engine/evd.ml index 6ba8a5112..7ee342ea0 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -383,8 +383,7 @@ let add_name_newly_undefined naming evk evi (evtoid, idtoev as names) = | Misctypes.IntroAnonymous -> None | Misctypes.IntroIdentifier id -> if Idmap.mem id idtoev then - user_err_loc - (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id); + user_err "" (str "Already an existential evar of name " ++ pr_id id); Some id | Misctypes.IntroFresh id -> let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in diff --git a/engine/uState.ml b/engine/uState.ml index c35f97b2e..c82c30400 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -255,8 +255,8 @@ let universe_context ?names ctx = let l = try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) with Not_found -> - user_err_loc (loc, "universe_context", - str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") + user_err ~loc "universe_context" + (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc)) pl ([], [], levels) in @@ -269,8 +269,8 @@ let universe_context ?names ctx = Option.default Loc.ghost info.uloc with Not_found -> Loc.ghost in - user_err_loc (loc, "universe_context", - (str(CString.plural n "Universe") ++ spc () ++ + user_err ~loc "universe_context" + ((str(CString.plural n "Universe") ++ spc () ++ Univ.LSet.pr (pr_uctx_level ctx) left ++ spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.")) diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 4046ef7ae..8dda4773e 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -96,7 +96,7 @@ let is_undo cmd = match cmd with (** Check whether a command is forbidden by CoqIDE *) let coqide_cmd_checks (loc,ast) = - let user_error s = CErrors.user_err_loc (loc, "CoqIde", str s) in + let user_error s = CErrors.user_err ~loc "CoqIde" (str s) in if is_debug ast then user_error "Debug mode not available within CoqIDE"; if is_known_option ast then diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 04429851f..9097a56f8 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -382,18 +382,18 @@ let rec prod_constr_expr c = function let coerce_reference_to_id = function | Ident (_,id) -> id | Qualid (loc,_) -> - CErrors.user_err_loc (loc, "coerce_reference_to_id", - str "This expression should be a simple identifier.") + CErrors.user_err ~loc "coerce_reference_to_id" + (str "This expression should be a simple identifier.") let coerce_to_id = function | CRef (Ident (loc,id),_) -> (loc,id) - | a -> CErrors.user_err_loc - (constr_loc a,"coerce_to_id", - str "This expression should be a simple identifier.") + | a -> CErrors.user_err ~loc:(constr_loc a) + "coerce_to_id" + (str "This expression should be a simple identifier.") let coerce_to_name = function | CRef (Ident (loc,id),_) -> (loc,Name id) | CHole (loc,_,_,_) -> (loc,Anonymous) - | a -> CErrors.user_err_loc - (constr_loc a,"coerce_to_name", - str "This expression should be a name.") + | a -> CErrors.user_err + ~loc:(constr_loc a) "coerce_to_name" + (str "This expression should be a name.") diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e71daef99..3e6bc80f2 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -94,8 +94,8 @@ let is_record indsp = let encode_record r = let indsp = global_inductive r in if not (is_record indsp) then - user_err_loc (loc_of_reference r,"encode_record", - str "This type is not a structure type."); + user_err ~loc:(loc_of_reference r) "encode_record" + (str "This type is not a structure type."); indsp module PrintingRecordRecord = diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7c4688f9f..f4907e92a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -154,17 +154,17 @@ let explain_internalization_error e = | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2 in pp ++ str "." -let error_bad_inductive_type loc = - user_err_loc (loc,"",str +let error_bad_inductive_type ?loc = + user_err ?loc "" (str "This should be an inductive type applied to patterns.") -let error_parameter_not_implicit loc = - user_err_loc (loc,"", str +let error_parameter_not_implicit ?loc = + user_err ?loc "" (str "The parameters do not bind in patterns;" ++ spc () ++ str "they must be replaced by '_'.") -let error_ldots_var loc = - user_err_loc (loc,"",str "Special token " ++ pr_id ldots_var ++ +let error_ldots_var ?loc = + user_err ?loc "" (str "Special token " ++ pr_id ldots_var ++ str " is for use in the Notation command.") (**********************************************************************) @@ -262,15 +262,15 @@ let pr_scope_stack = function | l -> str "scope stack " ++ str "[" ++ prlist_with_sep pr_comma str l ++ str "]" -let error_inconsistent_scope loc id scopes1 scopes2 = - user_err_loc (loc,"set_var_scope", - pr_id id ++ str " is here used in " ++ +let error_inconsistent_scope ?loc id scopes1 scopes2 = + user_err ?loc "set_var_scope" + (pr_id id ++ str " is here used in " ++ pr_scope_stack scopes2 ++ strbrk " while it was elsewhere used in " ++ pr_scope_stack scopes1) -let error_expect_binder_notation_type loc id = - user_err_loc (loc,"", - pr_id id ++ +let error_expect_binder_notation_type ?loc id = + user_err ?loc "" + (pr_id id ++ str " is expected to occur in binding position in the right-hand side.") let set_var_scope loc id istermvar env ntnvars = @@ -284,12 +284,12 @@ let set_var_scope loc id istermvar env ntnvars = | Some (tmp, scope) -> let s1 = make_current_scope tmp scope in let s2 = make_current_scope env.tmp_scope env.scopes in - if not (List.equal String.equal s1 s2) then error_inconsistent_scope loc id s1 s2 + if not (List.equal String.equal s1 s2) then error_inconsistent_scope ~loc id s1 s2 end in match typ with | NtnInternTypeBinder -> - if istermvar then error_expect_binder_notation_type loc id + if istermvar then error_expect_binder_notation_type ~loc id | NtnInternTypeConstr -> (* We need sometimes to parse idents at a constr level for factorization and we cannot enforce this constraint: @@ -373,12 +373,12 @@ let push_name_env ?(global_level=false) ntnvars implargs env = function | loc,Anonymous -> if global_level then - user_err_loc (loc,"", str "Anonymous variables not allowed"); + user_err ~loc "" (str "Anonymous variables not allowed"); env | loc,Name id -> check_hidden_implicit_parameters id env.impls ; if Id.Map.is_empty ntnvars && Id.equal id ldots_var - then error_ldots_var loc; + then error_ldots_var ~loc; set_var_scope loc id false env ntnvars; if global_level then Dumpglob.dump_definition (loc,id) true "var" else Dumpglob.dump_binding loc id; @@ -764,7 +764,7 @@ let string_of_ty = function let gvar (loc, id) us = match us with | None -> GVar (loc, id) | Some _ -> - user_err_loc (loc, "", str "Variable " ++ pr_id id ++ + user_err ~loc "" (str "Variable " ++ pr_id id ++ str " cannot have a universe instance") let intern_var genv (ltacvars,ntnvars) namedctx loc id us = @@ -788,12 +788,12 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us = (* Is [id] the special variable for recursive notations *) else if Id.equal id ldots_var then if Id.Map.is_empty ntnvars - then error_ldots_var loc + then error_ldots_var ~loc else gvar (loc,id) us, [], [], [] else if Id.Set.mem id ltacvars.ltac_bound then (* Is [id] bound to a free name in ltac (this is an ltac error message) *) - user_err_loc (loc,"intern_var", - str "variable " ++ pr_id id ++ str " should be bound to a term.") + user_err ~loc "intern_var" + (str "variable " ++ pr_id id ++ str " should be bound to a term.") else (* Is [id] a goal or section variable *) let _ = Context.Named.lookup id namedctx in @@ -825,7 +825,7 @@ let find_appl_head_data c = | x -> x,[],[],[] let error_not_enough_arguments loc = - user_err_loc (loc,"",str "Abbreviation is not applied enough.") + user_err ~loc "" (str "Abbreviation is not applied enough.") let check_no_explicitation l = let is_unset (a, b) = match b with None -> false | Some _ -> true in @@ -834,7 +834,7 @@ let check_no_explicitation l = | [] -> () | (_, None) :: _ -> assert false | (_, Some (loc, _)) :: _ -> - user_err_loc (loc,"",str"Unexpected explicitation of the argument of an abbreviation.") + user_err ~loc "" (str"Unexpected explicitation of the argument of an abbreviation.") let dump_extended_global loc = function | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob loc ref @@ -847,7 +847,7 @@ let intern_reference ref = let qid = qualid_of_reference ref in let r = try intern_extended_global_of_qualid qid - with Not_found -> error_global_not_found_loc (fst qid) (snd qid) + with Not_found -> error_global_not_found ~loc:(fst qid) (snd qid) in Smartlocate.global_of_extended_global r @@ -872,7 +872,7 @@ let intern_qualid loc qid intern env lvar us args = | Some _, GApp (loc, GRef (loc', ref, None), arg) -> GApp (loc, GRef (loc', ref, us), arg) | Some _, _ -> - user_err_loc (loc, "", str "Notation " ++ pr_qualid qid ++ + user_err ~loc "" (str "Notation " ++ pr_qualid qid ++ str " cannot have a universe instance, its expanded head does not start with a reference") in @@ -888,7 +888,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = | Qualid (loc, qid) -> let r,projapp,args2 = try intern_qualid loc qid intern env ntnvars us args - with Not_found -> error_global_not_found_loc loc qid + with Not_found -> error_global_not_found ~loc qid in let x, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), args2 @@ -904,7 +904,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then (gvar (loc,id) us, [], [], []), args - else error_global_not_found_loc loc qid + else error_global_not_found ~loc qid let interp_reference vars r = let (r,_,_,_),_ = @@ -982,7 +982,7 @@ let check_number_of_pattern loc n l = let check_or_pat_variables loc ids idsl = if List.exists (fun ids' -> not (List.eq_set Id.equal ids ids')) idsl then - user_err_loc (loc, "", str + user_err ~loc "" (str "The components of this disjunctive pattern must bind the same variables.") (** Use only when params were NOT asked to the user. @@ -991,7 +991,7 @@ let check_constructor_length env loc cstr len_pl pl0 = let n = len_pl + List.length pl0 in if Int.equal n (Inductiveops.constructor_nallargs cstr) then false else (Int.equal n (Inductiveops.constructor_nalldecls cstr) || - (error_wrong_numarg_constructor_loc loc env cstr + (error_wrong_numarg_constructor ~loc env cstr (Inductiveops.constructor_nrealargs cstr))) let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 = @@ -1016,14 +1016,14 @@ let add_implicits_check_constructor_length env loc c len_pl1 pl2 = let nargs = Inductiveops.constructor_nallargs c in let nargs' = Inductiveops.constructor_nalldecls c in let impls_st = implicits_of_global (ConstructRef c) in - add_implicits_check_length (error_wrong_numarg_constructor_loc loc env c) + add_implicits_check_length (error_wrong_numarg_constructor ~loc env c) nargs nargs' impls_st len_pl1 pl2 let add_implicits_check_ind_length env loc c len_pl1 pl2 = let nallargs = inductive_nallargs_env env c in let nalldecls = inductive_nalldecls_env env c in let impls_st = implicits_of_global (IndRef c) in - add_implicits_check_length (error_wrong_numarg_inductive_loc loc env c) + add_implicits_check_length (error_wrong_numarg_inductive ~loc env c) nallargs nalldecls impls_st len_pl1 pl2 (** Do not raise NotEnoughArguments thanks to preconditions*) @@ -1034,7 +1034,7 @@ let chop_params_pattern loc ind args with_letin = assert (nparams <= List.length args); let params,args = List.chop nparams args in List.iter (function PatVar(_,Anonymous) -> () - | PatVar (loc',_) | PatCstr(loc',_,_,_) -> error_parameter_not_implicit loc') params; + | PatVar (loc',_) | PatCstr(loc',_,_,_) -> error_parameter_not_implicit ~loc:loc') params; args let find_constructor loc add_params ref = @@ -1042,10 +1042,10 @@ let find_constructor loc add_params ref = | ConstructRef cstr -> cstr | IndRef _ -> let error = str "There is an inductive name deep in a \"in\" clause." in - user_err_loc (loc, "find_constructor", error) + user_err ~loc "find_constructor" error | ConstRef _ | VarRef _ -> let error = str "This reference is not a constructor." in - user_err_loc (loc, "find_constructor", error) + user_err ~loc "find_constructor" error in cstr, match add_params with | Some nb_args -> @@ -1085,8 +1085,8 @@ let sort_fields ~complete loc fields completer = let record = try Recordops.find_projection first_field_glob_ref with Not_found -> - user_err_loc (loc_of_reference first_field_ref, "intern", - pr_reference first_field_ref ++ str": Not a projection") + user_err ~loc:(loc_of_reference first_field_ref) "intern" + (pr_reference first_field_ref ++ str": Not a projection") in (* the number of parameters *) let nparams = record.Recordops.s_EXPECTEDPARAM in @@ -1114,7 +1114,7 @@ let sort_fields ~complete loc fields completer = by a let-in in the record declaration (its value is fixed from other fields). *) if first_field && not regular && complete then - user_err_loc (loc, "", str "No local fields allowed in a record construction.") + user_err ~loc "" (str "No local fields allowed in a record construction.") else if first_field then build_proj_list projs proj_kinds (idx+1) ~acc_first_idx:idx acc else if not regular && complete then @@ -1127,7 +1127,7 @@ let sort_fields ~complete loc fields completer = | None :: projs -> if complete then (* we don't want anonymous fields *) - user_err_loc (loc, "", str "This record contains anonymous fields.") + user_err ~loc "" (str "This record contains anonymous fields.") else (* anonymous arguments don't appear in proj_kinds *) build_proj_list projs proj_kinds (idx+1) ~acc_first_idx acc @@ -1141,15 +1141,14 @@ let sort_fields ~complete loc fields completer = | (field_ref, field_value) :: fields -> let field_glob_ref = try global_reference_of_reference field_ref with Not_found -> - user_err_loc (loc_of_reference field_ref, "intern", - str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in + user_err ~loc:(loc_of_reference field_ref) "intern" + (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in let remaining_projs, (field_index, _) = let the_proj (idx, glob_ref) = eq_gr field_glob_ref glob_ref in try CList.extract_first the_proj remaining_projs with Not_found -> - user_err_loc - (loc, "", - str "This record contains fields of different records.") + user_err ~loc "" + (str "This record contains fields of different records.") in index_fields fields remaining_projs ((field_index, field_value) :: acc) | [] -> @@ -1220,7 +1219,7 @@ let drop_notations_pattern looked_for = if top then looked_for g else match g with ConstructRef _ -> () | _ -> raise Not_found with Not_found -> - error_invalid_pattern_notation loc + error_invalid_pattern_notation ~loc in let test_kind top = if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found @@ -1345,8 +1344,8 @@ let drop_notations_pattern looked_for = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @ List.map (in_pat false scopes) args, []) | NList (x,y,iter,terminator,lassoc) -> - if not (List.is_empty args) then user_err_loc - (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns."); + if not (List.is_empty args) then user_err ~loc "" + (strbrk "Application of arguments to a recursive notation not supported in patterns."); (try (* All elements of the list are in scopes (scopt,subscopes) *) let (l,(scopt,subscopes)) = Id.Map.find x substlist in @@ -1361,7 +1360,7 @@ let drop_notations_pattern looked_for = | NHole _ -> let () = assert (List.is_empty args) in RCPatAtom (loc, None) - | t -> error_invalid_pattern_notation loc + | t -> error_invalid_pattern_notation ~loc in in_pat true let rec intern_pat genv aliases pat = @@ -1413,11 +1412,11 @@ let intern_ind_pattern genv scopes pat = let no_not = try drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat - with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type loc + with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ~loc in match no_not with | RCPatCstr (loc, head, expl_pl, pl) -> - let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type loc) head in + let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ~loc) head in let with_letin, pl2 = add_implicits_check_ind_length genv loc c (List.length expl_pl) pl in let idslpl1 = List.rev_map (intern_pat genv empty_alias) expl_pl in @@ -1425,8 +1424,8 @@ let intern_ind_pattern genv scopes pat = (with_letin, match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin) - | _ -> error_bad_inductive_type loc) - | x -> error_bad_inductive_type (raw_cases_pattern_expr_loc x) + | _ -> error_bad_inductive_type ~loc) + | x -> error_bad_inductive_type ~loc:(raw_cases_pattern_expr_loc x) (**********************************************************************) (* Utilities for application *) @@ -1465,10 +1464,10 @@ let extract_explicit_arg imps args = let id = match pos with | ExplByName id -> if not (exists_implicit_name id imps) then - user_err_loc - (loc,"",str "Wrong argument name: " ++ pr_id id ++ str "."); + user_err ~loc "" + (str "Wrong argument name: " ++ pr_id id ++ str "."); if Id.Map.mem id eargs then - user_err_loc (loc,"",str "Argument name " ++ pr_id id + user_err ~loc "" (str "Argument name " ++ pr_id id ++ str " occurs more than once."); id | ExplByPos (p,_id) -> @@ -1478,11 +1477,11 @@ let extract_explicit_arg imps args = if not (is_status_implicit imp) then failwith "imp"; name_of_implicit imp with Failure _ (* "nth" | "imp" *) -> - user_err_loc - (loc,"",str"Wrong argument position: " ++ int p ++ str ".") + user_err ~loc "" + (str"Wrong argument position: " ++ int p ++ str ".") in if Id.Map.mem id eargs then - user_err_loc (loc,"",str"Argument at position " ++ int p ++ + user_err ~loc "" (str"Argument at position " ++ int p ++ str " is mentioned more than once."); id in (Id.Map.add id (loc, a) eargs, rargs) @@ -1533,7 +1532,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = (function | BDRawDef a -> a | BDPattern (loc,_,_,_,_) -> - Loc.raise loc (Stream.Error "pattern with quote not allowed after fix")) rbl in + Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")) rbl in ((n, ro), bl, intern_type env' ty, env')) dl in let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') -> let env'' = List.fold_left_i (fun i en name -> @@ -1637,7 +1636,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = in begin match fields with - | None -> user_err_loc (loc, "intern", str"No constructor inference.") + | None -> user_err ~loc "intern" (str"No constructor inference.") | Some (n, constrname, args) -> let pars = List.make n (CHole (loc, None, Misctypes.IntroAnonymous, None)) in let app = CAppExpl (loc, (None, constrname,None), List.rev_append pars args) in @@ -1860,7 +1859,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = | (imp::impl', []) -> if not (Id.Map.is_empty eargs) then (let (id,(loc,_)) = Id.Map.choose eargs in - user_err_loc (loc,"",str "Not enough non implicit \ + user_err ~loc "" (str "Not enough non implicit \ arguments to accept the argument bound to " ++ pr_id id ++ str".")); [] @@ -1891,8 +1890,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = intern env c with InternalizationError (loc,e) -> - user_err_loc (loc,"internalize", - explain_internalization_error e) + user_err ~loc "internalize" + (explain_internalization_error e) (**************************************************************************) (* Functions to translate constr_expr into glob_constr *) @@ -1931,7 +1930,7 @@ let intern_pattern globalenv patt = intern_cases_pattern globalenv (None,[]) empty_alias patt with InternalizationError (loc,e) -> - user_err_loc (loc,"internalize",explain_internalization_error e) + user_err ~loc "internalize" (explain_internalization_error e) (*********************************************************************) @@ -2042,13 +2041,13 @@ let intern_context global_level env impl_env binders = (function | BDRawDef a -> a | BDPattern (loc,_,_,_,_) -> - Loc.raise loc (Stream.Error "pattern with quote not allowed here")) bl in + Loc.raise ~loc (Stream.Error "pattern with quote not allowed here")) bl in (env, bl)) ({ids = extract_ids env; unb = false; tmp_scope = None; scopes = []; impls = impl_env}, []) binders in (lenv.impls, List.map snd bl) with InternalizationError (loc,e) -> - user_err_loc (loc,"internalize", explain_internalization_error e) + user_err ~loc "internalize" (explain_internalization_error e) let interp_rawcontext_evars env evdref k bl = let (env, par, _, impls) = diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 10cfbe58f..8908e1f6f 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -27,12 +27,12 @@ let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident" let declare_generalizable_ident table (loc,id) = if not (Id.equal id (root_of_id id)) then - user_err_loc(loc,"declare_generalizable_ident", - (pr_id id ++ str + user_err ~loc "declare_generalizable_ident" + ((pr_id id ++ str " is not declarable as generalizable identifier: it must have no trailing digits, quote, or _")); if Id.Pred.mem id table then - user_err_loc(loc,"declare_generalizable_ident", - (pr_id id++str" is already declared as a generalizable identifier")) + user_err ~loc "declare_generalizable_ident" + ((pr_id id++str" is already declared as a generalizable identifier")) else Id.Pred.add id table let add_generalizable gen table = @@ -78,8 +78,8 @@ let is_freevar ids env x = (* Auxiliary functions for the inference of implicitly quantified variables. *) let ungeneralizable loc id = - user_err_loc (loc, "Generalization", - str "Unbound and ungeneralizable variable " ++ pr_id id) + user_err ~loc "Generalization" + (str "Unbound and ungeneralizable variable " ++ pr_id id) let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let found loc id bdvars l = @@ -203,7 +203,7 @@ let combine_params avoid fn applied needed = | Anonymous -> false in if not (List.exists is_id needed) then - user_err_loc (loc,"",str "Wrong argument name: " ++ Nameops.pr_id id); + user_err ~loc "" (str "Wrong argument name: " ++ Nameops.pr_id id); true | _ -> false) applied in @@ -237,7 +237,7 @@ let combine_params avoid fn applied needed = aux (t' :: ids) avoid' app need | (x,_) :: _, [] -> - user_err_loc (Constrexpr_ops.constr_loc x,"",str "Typeclass does not expect more arguments") + user_err ~loc:(Constrexpr_ops.constr_loc x) "" (str "Typeclass does not expect more arguments") in aux [] avoid applied needed let combine_params_freevar = diff --git a/interp/modintern.ml b/interp/modintern.ml index e5dce5ccf..d4ade7058 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -26,16 +26,16 @@ let error_not_a_module_loc kind loc qid = | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s) | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s) in - Loc.raise loc e + Loc.raise ~loc e let error_application_to_not_path loc me = - Loc.raise loc (Modops.ModuleTypingError (Modops.ApplicationToNotPath me)) + Loc.raise ~loc (Modops.ModuleTypingError (Modops.ApplicationToNotPath me)) let error_incorrect_with_in_module loc = - Loc.raise loc (ModuleInternalizationError IncorrectWithInModule) + Loc.raise ~loc (ModuleInternalizationError IncorrectWithInModule) let error_application_to_module_type loc = - Loc.raise loc (ModuleInternalizationError IncorrectModuleApplication) + Loc.raise ~loc (ModuleInternalizationError IncorrectModuleApplication) (** Searching for a module name in the Nametab. diff --git a/interp/notation.ml b/interp/notation.ml index 0798d385d..0c15e91b8 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -220,8 +220,8 @@ let remove_delimiters scope = let find_delimiters_scope loc key = try String.Map.find key !delimiters_map with Not_found -> - user_err_loc - (loc, "find_delimiters", str "Unknown scope delimiting key " ++ str key ++ str ".") + user_err ~loc "find_delimiters" + (str "Unknown scope delimiting key " ++ str key ++ str ".") (* Uninterpretation tables *) @@ -337,8 +337,8 @@ let declare_string_interpreter sc dir interp (patl,uninterp,inpat) = let check_required_module loc sc (sp,d) = try let _ = Nametab.global_of_path sp in () with Not_found -> - user_err_loc (loc,"prim_token_interpreter", - str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".") + user_err ~loc "prim_token_interpreter" + (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".") (* Look if some notation or numeral printer in [scope] can be used in the scope stack [scopes], and if yes, using delimiters or not *) @@ -458,8 +458,8 @@ let interp_prim_token_gen g loc p local_scopes = let p_as_ntn = try notation_of_prim_token p with Not_found -> "" in try find_interpretation p_as_ntn (find_prim_token g loc p) scopes with Not_found -> - user_err_loc (loc,"interp_prim_token", - (match p with + user_err ~loc "interp_prim_token" + ((match p with | Numeral n -> str "No interpretation for numeral " ++ str (to_string n) | String s -> str "No interpretation for string " ++ qs s) ++ str ".") @@ -483,8 +483,8 @@ let interp_notation loc ntn local_scopes = let scopes = make_current_scopes local_scopes in try find_interpretation ntn (find_notation ntn) scopes with Not_found -> - user_err_loc - (loc,"",str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".") + user_err ~loc "" + (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".") let uninterp_notations c = List.map_append (fun key -> keymap_find key !notations_key_table) @@ -890,11 +890,11 @@ let global_reference_of_notation test (ntn,(sc,c,_)) = | _ -> None let error_ambiguous_notation loc _ntn = - user_err_loc (loc,"",str "Ambiguous notation.") + user_err ~loc "" (str "Ambiguous notation.") let error_notation_not_reference loc ntn = - user_err_loc (loc,"", - str "Unable to interpret " ++ quote (str ntn) ++ + user_err ~loc "" + (str "Unable to interpret " ++ quote (str ntn) ++ str " as a reference.") let interp_notation_as_global_reference loc test ntn sc = @@ -1017,8 +1017,8 @@ let add_notation_extra_printing_rule ntn k v = let p, pp, gr = String.Map.find ntn !notation_rules in String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules with Not_found -> - user_err_loc (Loc.ghost,"add_notation_extra_printing_rule", - str "No such Notation.") + user_err "add_notation_extra_printing_rule" + (str "No such Notation.") (**********************************************************************) (* Synchronisation with reset *) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index f3e0682bd..7ab6ebb26 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -233,8 +233,8 @@ let split_at_recursive_part c = let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1) let check_is_hole id = function GHole _ -> () | t -> - user_err_loc (loc_of_glob_constr t,"", - strbrk "In recursive notation with binders, " ++ pr_id id ++ + user_err ~loc:(loc_of_glob_constr t) "" + (strbrk "In recursive notation with binders, " ++ pr_id id ++ strbrk " is expected to come without type.") let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' @@ -283,8 +283,8 @@ let compare_recursive_parts found f f' (iterator,subc) = let loc1 = loc_of_glob_constr iterator in let loc2 = loc_of_glob_constr (Option.get !terminator) in (* Here, we would need a loc made of several parts ... *) - user_err_loc (subtract_loc loc1 loc2,"", - str "Both ends of the recursive pattern are the same.") + user_err ~loc:(subtract_loc loc1 loc2) "" + (str "Both ends of the recursive pattern are the same.") | Some (x,y,Some lassoc) -> let newfound,x,y,lassoc = if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) || @@ -324,8 +324,8 @@ let notation_constr_and_vars_of_glob_constr a = | GApp (_,GVar (loc,f),[c]) when Id.equal f ldots_var -> (* Fall on the second part of the recursive pattern w/o having found the first part *) - user_err_loc (loc,"", - str "Cannot find where the recursive pattern starts.") + user_err ~loc "" + (str "Cannot find where the recursive pattern starts.") | c -> aux' c and aux' = function diff --git a/interp/reserve.ml b/interp/reserve.ml index 388ca0805..31425fb98 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -86,13 +86,13 @@ let in_reserved : Id.t * notation_constr -> obj = let declare_reserved_type_binding (loc,id) t = if not (Id.equal id (root_of_id id)) then - user_err_loc(loc,"declare_reserved_type", - (pr_id id ++ str + user_err ~loc "declare_reserved_type" + ((pr_id id ++ str " is not reservable: it must have no trailing digits, quote, or _")); begin try let _ = Id.Map.find id !reserve_table in - user_err_loc(loc,"declare_reserved_type", - (pr_id id++str" is already bound to a type")) + user_err ~loc "declare_reserved_type" + ((pr_id id++str" is already bound to a type")) with Not_found -> () end; add_anonymous_leaf (in_reserved (id,t)) diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 478774219..08425129b 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -46,7 +46,7 @@ let locate_global_with_alias ?(head=false) (loc,qid) = if head then global_of_extended_global_head ref else global_of_extended_global ref with Not_found -> - user_err_loc (loc,"",pr_qualid qid ++ + user_err ~loc "" (pr_qualid qid ++ str " is bound to a notation that does not denote a reference.") let global_inductive_with_alias r = @@ -54,14 +54,14 @@ let global_inductive_with_alias r = try match locate_global_with_alias lqid with | IndRef ind -> ind | ref -> - user_err_loc (loc_of_reference r,"global_inductive", - pr_reference r ++ spc () ++ str "is not an inductive type.") - with Not_found -> Nametab.error_global_not_found_loc loc qid + user_err ~loc:(loc_of_reference r) "global_inductive" + (pr_reference r ++ spc () ++ str "is not an inductive type.") + with Not_found -> Nametab.error_global_not_found ~loc qid let global_with_alias ?head r = let (loc,qid as lqid) = qualid_of_reference r in try locate_global_with_alias ?head lqid - with Not_found -> Nametab.error_global_not_found_loc loc qid + with Not_found -> Nametab.error_global_not_found ~loc qid let smart_global ?head = function | AN r -> diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 2b860173a..ed44e66ff 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -32,8 +32,8 @@ let _ = Goptions.declare_bool_option { (**********************************************************************) (* Miscellaneous *) -let error_invalid_pattern_notation loc = - user_err_loc (loc,"",str "Invalid notation for pattern.") +let error_invalid_pattern_notation ?loc = + user_err ?loc "" (str "Invalid notation for pattern.") (**********************************************************************) (* Functions on constr_expr *) @@ -175,8 +175,8 @@ let split_at_annot bl na = | LocalRawDef _ as x :: rest -> aux (x :: acc) rest | LocalPattern _ :: rest -> assert false | [] -> - user_err_loc(loc,"", - str "No parameter named " ++ Nameops.pr_id id ++ str".") + user_err ~loc "" + (str "No parameter named " ++ Nameops.pr_id id ++ str".") in aux [] bl (* Used in correctness and interface *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 58edd4ddf..ac98331c6 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -46,4 +46,4 @@ val patntn_loc : (** For cases pattern parsing errors *) -val error_invalid_pattern_notation : Loc.t -> 'a +val error_invalid_pattern_notation : ?loc:Loc.t -> 'a diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 1459141d1..c5f262373 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -26,9 +26,8 @@ let _ = let make_anomaly ?label pp = Anomaly (label, pp) -let anomaly ?loc ?label pp = match loc with - | None -> raise (Anomaly (label, pp)) - | Some loc -> Loc.raise loc (Anomaly (label, pp)) +let anomaly ?loc ?label pp = + Loc.raise ?loc (Anomaly (label, pp)) let is_anomaly = function | Anomaly _ -> true @@ -43,8 +42,8 @@ let alreadydeclared pps = raise (AlreadyDeclared(pps)) let todo s = prerr_string ("TODO: "^s^"\n") -let user_err_loc (loc,s,strm) = Loc.raise loc (UserError (s,strm)) -let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s) +let user_err ?loc s strm = Loc.raise ?loc (UserError (s,strm)) +let invalid_arg ?loc s = Loc.raise ?loc (Invalid_argument s) exception Timeout exception Drop diff --git a/lib/cErrors.mli b/lib/cErrors.mli index e5dad93fd..291c39b84 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -36,12 +36,13 @@ val is_anomaly : exn -> bool exception UserError of string * std_ppcmds val error : string -> 'a val errorlabstrm : string -> std_ppcmds -> 'a -val user_err_loc : Loc.t * string * std_ppcmds -> 'a + +val user_err : ?loc:Loc.t -> string -> std_ppcmds -> 'a exception AlreadyDeclared of std_ppcmds val alreadydeclared : std_ppcmds -> 'a -val invalid_arg_loc : Loc.t * string -> 'a +val invalid_arg : ?loc:Loc.t -> string -> 'a (** [todo] is for running of an incomplete code its implementation is "do nothing" (or print a message), but this function should not be diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 78fa84f33..f36c7ad80 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -45,7 +45,7 @@ let create ~name ~category ?(default=Enabled) pp = | Disabled -> () | AsError -> let loc = Option.default !current_loc loc in - CErrors.user_err_loc (loc,"_",pp x) + CErrors.user_err ~loc "_" (pp x) | Enabled -> let msg = pp x ++ spc () ++ str "[" ++ str name ++ str "," ++ diff --git a/lib/loc.ml b/lib/loc.ml index 0f9864a9a..e373a760c 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -71,6 +71,9 @@ let add_loc e loc = Exninfo.add e location loc let get_loc e = Exninfo.get e location -let raise loc e = - let info = Exninfo.add Exninfo.null location loc in - Exninfo.iraise (e, info) +let raise ?loc e = + match loc with + | None -> raise e + | Some loc -> + let info = Exninfo.add Exninfo.null location loc in + Exninfo.iraise (e, info) diff --git a/lib/loc.mli b/lib/loc.mli index c08e097a8..bb88f8642 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -51,7 +51,7 @@ val add_loc : Exninfo.info -> t -> Exninfo.info val get_loc : Exninfo.info -> t option (** Retrieving the optional location of an exception *) -val raise : t -> exn -> 'a +val raise : ?loc:t -> exn -> 'a (** [raise loc e] is the same as [Pervasives.raise (add_loc e loc)]. *) (** {5 Location utilities} *) diff --git a/library/declare.ml b/library/declare.ml index 3d063225f..f8c3cddc4 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -462,8 +462,8 @@ let do_universe poly l = let in_section = Lib.sections_are_opened () in let () = if poly && not in_section then - user_err_loc (Loc.ghost, "Constraint", - str"Cannot declare polymorphic universes outside sections") + user_err "Constraint" + (str"Cannot declare polymorphic universes outside sections") in let l = List.map (fun (l, id) -> @@ -496,20 +496,20 @@ let do_constraint poly l = fun (loc, id) -> try Idmap.find id names with Not_found -> - user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) + user_err ~loc "Constraint" (str "Undeclared universe " ++ pr_id id) in let in_section = Lib.sections_are_opened () in let () = if poly && not in_section then - user_err_loc (Loc.ghost, "Constraint", - str"Cannot declare polymorphic constraints outside sections") + user_err "Constraint" + (str"Cannot declare polymorphic constraints outside sections") in let check_poly loc p loc' p' = if poly then () else if p || p' then let loc = if p then loc else loc' in - user_err_loc (loc, "Constraint", - str "Cannot declare a global constraint on " ++ + user_err ~loc "Constraint" + (str "Cannot declare a global constraint on " ++ str "a polymorphic universe, use " ++ str "Polymorphic Constraint instead") in diff --git a/library/library.ml b/library/library.ml index 12090183a..0d65b3d0a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -572,8 +572,8 @@ let require_library_from_dirpath modrefl export = let safe_locate_module (loc,qid) = try Nametab.locate_module qid with Not_found -> - user_err_loc - (loc,"import_library", pr_qualid qid ++ str " is not a module") + user_err ~loc "import_library" + (pr_qualid qid ++ str " is not a module") let import_module export modl = (* Optimization: libraries in a raw in the list are imported @@ -597,8 +597,8 @@ let import_module export modl = flush acc; try Declaremods.import_module export mp; aux [] l with Not_found -> - user_err_loc (loc,"import_library", - pr_qualid dir ++ str " is not a module")) + user_err ~loc "import_library" + (pr_qualid dir ++ str " is not a module")) | [] -> flush acc in aux [] modl diff --git a/library/nametab.ml b/library/nametab.ml index fa5db37ed..989dcf3f3 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -16,10 +16,8 @@ open Globnames exception GlobalizationError of qualid -let error_global_not_found_loc loc q = - Loc.raise loc (GlobalizationError q) - -let error_global_not_found q = raise (GlobalizationError q) +let error_global_not_found ?loc q = + Loc.raise ?loc (GlobalizationError q) (* Kinds of global names *) @@ -455,11 +453,11 @@ let global r = try match locate_extended qid with | TrueGlobal ref -> ref | SynDef _ -> - user_err_loc (loc,"global", - str "Unexpected reference to a notation: " ++ - pr_qualid qid) + user_err ~loc "global" + (str "Unexpected reference to a notation: " ++ + pr_qualid qid) with Not_found -> - error_global_not_found_loc loc qid + error_global_not_found ~loc qid (* Exists functions ********************************************************) @@ -534,8 +532,8 @@ let global_inductive r = match global r with | IndRef ind -> ind | ref -> - user_err_loc (loc_of_reference r,"global_inductive", - pr_reference r ++ spc () ++ str "is not an inductive type") + user_err ~loc:(loc_of_reference r) "global_inductive" + (pr_reference r ++ spc () ++ str "is not an inductive type") (********************************************************************) diff --git a/library/nametab.mli b/library/nametab.mli index a8a0572b3..d20c399b6 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -60,8 +60,7 @@ open Globnames exception GlobalizationError of qualid (** Raises a globalization error *) -val error_global_not_found_loc : Loc.t -> qualid -> 'a -val error_global_not_found : qualid -> 'a +val error_global_not_found : ?loc:Loc.t -> qualid -> 'a (** {6 Register visibility of things } *) diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index 9f2c0a93e..85f1a0225 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -36,8 +36,8 @@ let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c let reference_to_id = function | Libnames.Ident (loc, id) -> (loc, id) | Libnames.Qualid (loc,_) -> - CErrors.user_err_loc (loc, "", - str "This expression should be a simple identifier.") + CErrors.user_err ~loc "" + (str "This expression should be a simple identifier.") let tactic_mode = Gram.entry_create "vernac:tactic_command" diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 673ac832a..1b7430c3f 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -429,8 +429,8 @@ let register_ltac local tacl = let kn = Lib.make_kn id in let id_pp = pr_id id in let () = if is_defined_tac kn then - CErrors.user_err_loc (loc, "", - str "There is already an Ltac named " ++ id_pp ++ str".") + CErrors.user_err ~loc "" + (str "There is already an Ltac named " ++ id_pp ++ str".") in let is_shadowed = try @@ -446,8 +446,8 @@ let register_ltac local tacl = let kn = try Nametab.locate_tactic (snd (qualid_of_reference ident)) with Not_found -> - CErrors.user_err_loc (loc, "", - str "There is no Ltac named " ++ pr_reference ident ++ str ".") + CErrors.user_err ~loc "" + (str "There is no Ltac named " ++ pr_reference ident ++ str ".") in UpdateTac kn, body in diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index c5bb0ed07..dc216da11 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -32,11 +32,8 @@ open Locus let dloc = Loc.ghost -let error_global_not_found_loc (loc,qid) = - error_global_not_found_loc loc qid - -let error_tactic_expected loc = - user_err_loc (loc,"",str "Tactic expected.") +let error_tactic_expected ?loc = + user_err ?loc "" (str "Tactic expected.") (** Generic arguments *) @@ -85,7 +82,7 @@ let intern_hyp ist (loc,id as locid) = else if find_ident id ist then (dloc,id) else - Pretype_errors.error_var_not_found_loc loc id + Pretype_errors.error_var_not_found ~loc id let intern_or_var f ist = function | ArgVar locid -> ArgVar (intern_hyp ist locid) @@ -99,7 +96,7 @@ let intern_global_reference ist = function | r -> let loc,_ as lqid = qualid_of_reference r in try ArgArg (loc,locate_global_with_alias lqid) - with Not_found -> error_global_not_found_loc lqid + with Not_found -> error_global_not_found (snd lqid) let intern_ltac_variable ist = function | Ident (loc,id) -> @@ -143,7 +140,7 @@ let intern_isolated_tactic_reference strict ist r = try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) with Not_found -> (* Reference not found *) - error_global_not_found_loc (qualid_of_reference r) + error_global_not_found (snd (qualid_of_reference r)) (* Internalize an applied tactic reference *) @@ -159,7 +156,7 @@ let intern_applied_tactic_reference ist r = try intern_applied_global_tactic_reference r with Not_found -> (* Reference not found *) - error_global_not_found_loc (qualid_of_reference r) + error_global_not_found (snd (qualid_of_reference r)) (* Intern a reference parsed in a non-tactic entry *) @@ -180,7 +177,7 @@ let intern_non_tactic_reference strict ist r = TacGeneric ipat | _ -> (* Reference not found *) - error_global_not_found_loc (qualid_of_reference r) + error_global_not_found (snd (qualid_of_reference r)) let intern_message_token ist = function | (MsgString _ | MsgInt _ as x) -> x @@ -291,7 +288,7 @@ let intern_evaluable_global_reference ist r = with Not_found -> match r with | Ident (loc,id) when not !strict_check -> EvalVarRef id - | _ -> error_global_not_found_loc lqid + | _ -> error_global_not_found (snd lqid) let intern_evaluable_reference_or_by_notation ist = function | AN r -> intern_evaluable_global_reference ist r @@ -463,8 +460,8 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function (* Utilities *) let extract_let_names lrc = let fold accu ((loc, name), _) = - if Id.Set.mem name accu then user_err_loc - (loc, "glob_tactic", str "This variable is bound several times.") + if Id.Set.mem name accu then user_err ~loc + "glob_tactic" (str "This variable is bound several times.") else Id.Set.add name accu in List.fold_left fold Id.Set.empty lrc @@ -641,7 +638,7 @@ and intern_tactic_as_arg loc onlytac ist a = | TacGeneric _ as a -> TacArg (loc,a) | Tacexp a -> a | ConstrMayEval _ | TacFreshId _ | TacPretype _ | TacNumgoals as a -> - if onlytac then error_tactic_expected loc else TacArg (loc,a) + if onlytac then error_tactic_expected ~loc else TacArg (loc,a) and intern_tactic_or_tacarg ist = intern_tactic false ist diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index aa7e096a9..76c46ea7c 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -315,8 +315,8 @@ let append_trace trace v = (* Dynamically check that an argument is a tactic *) let coerce_to_tactic loc id v = let v = Value.normalize v in - let fail () = user_err_loc - (loc, "", str "Variable " ++ pr_id id ++ str " should be bound to a tactic.") + let fail () = user_err ~loc "" + (str "Variable " ++ pr_id id ++ str " should be bound to a tactic.") in let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then @@ -371,7 +371,7 @@ let debugging_exception_step ist signal_anomaly e pp = pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e) let error_ltac_variable loc id env v s = - user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++ + user_err ~loc "" (str "Ltac variable " ++ pr_id id ++ strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ strbrk "which cannot be coerced to " ++ str s ++ str".") @@ -404,8 +404,8 @@ let interp_intro_pattern_naming_var loc ist env sigma id = let interp_int ist locid = try try_interp_ltac_var coerce_to_int ist None locid with Not_found -> - user_err_loc(fst locid,"interp_int", - str "Unbound variable " ++ pr_id (snd locid) ++ str".") + user_err ~loc:(fst locid) "interp_int" + (str "Unbound variable " ++ pr_id (snd locid) ++ str".") let interp_int_or_var ist = function | ArgVar locid -> interp_int ist locid @@ -427,7 +427,7 @@ let interp_hyp ist env sigma (loc,id as locid) = with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id - else Loc.raise loc (Logic.RefinerError (Logic.NoSuchHyp id)) + else Loc.raise ~loc (Logic.RefinerError (Logic.NoSuchHyp id)) let interp_hyp_list_as_list ist env sigma (loc,id as x) = try coerce_to_hyp_list env (Id.Map.find id ist.lfun) @@ -449,7 +449,7 @@ let interp_reference ist env sigma = function with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) - with Not_found -> error_global_not_found_loc loc (qualid_of_ident id) + with Not_found -> error_global_not_found ~loc (qualid_of_ident id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in @@ -465,14 +465,14 @@ let interp_evaluable ist env sigma = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> error_global_not_found_loc loc (qualid_of_ident id) + | _ -> error_global_not_found ~loc (qualid_of_ident id) end | ArgArg (r,None) -> r | ArgVar (loc, id) -> try try_interp_ltac_var (coerce_to_evaluable_ref env) ist (Some (env,sigma)) (loc, id) with Not_found -> try try_interp_evaluable env (loc, id) - with Not_found -> error_global_not_found_loc loc (qualid_of_ident id) + with Not_found -> error_global_not_found ~loc (qualid_of_ident id) (* Interprets an hypothesis name *) let interp_occurrences ist occs = @@ -739,7 +739,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = Inr (pattern_of_constr env sigma c) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id) with Not_found -> - error_global_not_found_loc loc (qualid_of_ident id)) + error_global_not_found ~loc (qualid_of_ident id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p @@ -795,8 +795,8 @@ let interp_may_eval f ist env sigma = function !evdref , c with | Not_found -> - user_err_loc (loc, "interp_may_eval", - str "Unbound context identifier" ++ pr_id s ++ str".")) + user_err ~loc "interp_may_eval" + (str "Unbound context identifier" ++ pr_id s ++ str".")) | ConstrTypeOf c -> let (sigma,c_interp) = f ist env sigma c in Typing.type_of ~refresh:true env sigma c_interp @@ -1032,8 +1032,8 @@ let interp_destruction_arg ist gl arg = } | keep,ElimOnAnonHyp n as x -> x | keep,ElimOnIdent (loc,id) -> - let error () = user_err_loc (loc, "", - strbrk "Cannot coerce " ++ pr_id id ++ + let error () = user_err ~loc "" + (strbrk "Cannot coerce " ++ pr_id id ++ strbrk " neither to a quantified hypothesis nor to a term.") in let try_cast_id id' = @@ -1043,7 +1043,7 @@ let interp_destruction_arg ist gl arg = (keep, ElimOnConstr { delayed = begin fun env sigma -> try Sigma.here (constr_of_id env id', NoBindings) sigma with Not_found -> - user_err_loc (loc, "interp_destruction_arg", + user_err ~loc "interp_destruction_arg" ( pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.") end }) in @@ -1111,7 +1111,7 @@ let read_pattern lfun ist env sigma = function (* Reads the hypotheses of a Match Context rule *) let cons_and_check_name id l = if Id.List.mem id l then - user_err_loc (dloc,"read_match_goal_hyps", + user_err "read_match_goal_hyps" ( str "Hypothesis pattern-matching variable " ++ pr_id id ++ str " used twice in the same pattern.") else id::l diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 2acccfdf5..fadc5d113 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -106,7 +106,7 @@ let current_file = ref "" let set_current_file ~fname = current_file := fname -let err loc str = Loc.raise (Compat.to_coqloc loc) (Error.E str) +let err loc str = Loc.raise ~loc:(Compat.to_coqloc loc) (Error.E str) let bad_token str = raise (Error.E (Bad_token str)) diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index 18bc8d664..170dd7c55 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -188,7 +188,7 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct with Exc_located (loc,e) -> let loc' = Loc.get_loc (Exninfo.info e) in let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in - Loc.raise loc e + Loc.raise ~loc e let entry_print ft x = Entry.print ft x let srules' = Gramext.srules diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 74994c5e3..92a59be43 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -55,9 +55,9 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) = let mk_cofixb (id,bl,ann,body,(loc,tyc)) = let _ = Option.map (fun (aloc,_) -> - CErrors.user_err_loc - (aloc,"Constr:mk_cofixb", - Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in + CErrors.user_err ~loc:aloc + "Constr:mk_cofixb" + (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in let ty = match tyc with Some ty -> ty | None -> CHole (loc, None, IntroAnonymous, None) in @@ -380,14 +380,14 @@ GEXTEND Gram [ p = pattern; lp = LIST1 NEXT -> (match p with | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, None, lp) - | CPatCstr (_, r, None, l2) -> CErrors.user_err_loc - (cases_pattern_expr_loc p, "compound_pattern", - Pp.str "Nested applications not supported.") + | CPatCstr (_, r, None, l2) -> CErrors.user_err + ~loc:(cases_pattern_expr_loc p) "compound_pattern" + (Pp.str "Nested applications not supported.") | CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp) | CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp) - | _ -> CErrors.user_err_loc - (cases_pattern_expr_loc p, "compound_pattern", - Pp.str "Such pattern cannot have arguments.")) + | _ -> CErrors.user_err + ~loc:(cases_pattern_expr_loc p) "compound_pattern" + (Pp.str "Such pattern cannot have arguments.")) |"@"; r = Prim.reference; lp = LIST0 NEXT -> CPatCstr (!@loc, r, Some lp, []) ] | "1" LEFTA diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index b90e06cd3..b447a5de5 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -28,7 +28,7 @@ let my_int_of_string loc s = if n > 1024 * 2048 then raise Exit; n with Failure _ | Exit -> - CErrors.user_err_loc (loc,"",Pp.str "Cannot support a so large number.") + CErrors.user_err ~loc "" (Pp.str "Cannot support a so large number.") GEXTEND Gram GLOBAL: @@ -93,7 +93,7 @@ GEXTEND Gram ; ne_string: [ [ s = STRING -> - if s="" then CErrors.user_err_loc(!@loc, "", Pp.str"Empty string."); s + if s="" then CErrors.user_err ~loc:(!@loc) "" (Pp.str"Empty string."); s ] ] ; ne_lstring: diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 199ef9fce..2cc2b01c0 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -135,9 +135,9 @@ let mk_fix_tac (loc,id,bl,ann,ty) = let mk_cofix_tac (loc,id,bl,ann,ty) = let _ = Option.map (fun (aloc,_) -> - user_err_loc - (aloc,"Constr:mk_cofix_tac", - Pp.str"Annotation forbidden in cofix expression.")) ann in + user_err ~loc:aloc + "Constr:mk_cofix_tac" + (Pp.str"Annotation forbidden in cofix expression.")) ann in (id,CProdN(loc,bl,ty)) (* Functions overloaded by quotifier *) @@ -192,7 +192,7 @@ let merge_occurrences loc cl = function | None -> if Locusops.clause_with_generic_occurrences cl then (None, cl) else - user_err_loc (loc,"",str "Found an \"at\" clause without \"with\" clause.") + user_err ~loc "" (str "Found an \"at\" clause without \"with\" clause.") | Some (occs, p) -> let ans = match occs with | AllOccurrences -> cl @@ -204,9 +204,9 @@ let merge_occurrences loc cl = function { cl with onhyps = Some [(occs, id), l] } | _ -> if Locusops.clause_with_generic_occurrences cl then - user_err_loc (loc,"",str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.") + user_err ~loc "" (str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.") else - user_err_loc (loc,"",str "Cannot use clause \"at\" twice.") + user_err ~loc "" (str "Cannot use clause \"at\" twice.") end in (Some p, ans) diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index a862423e9..49843d828 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -90,7 +90,7 @@ let rec add_vars_of_simple_pattern globs = function (* Loc.raise loc (UserError ("simple_pattern",str "\"as\" is not allowed here"))*) | CPatOr (loc, _)-> - Loc.raise loc + Loc.raise ~loc (UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here")) | CPatDelimiters (_,_,p) -> add_vars_of_simple_pattern globs p diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 18817f504..4f183b3a1 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -175,7 +175,7 @@ let build_newrecursive l = match body_opt with | Some body -> (fixna,bll,ar,body) - | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") + | None -> user_err "Function" (str "Body of Function must be given") ) l in build_newrecursive l' @@ -391,7 +391,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = match fixpoint_exprl with | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec -> - let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err "Function" (str "Body of Function must be given") in Command.do_definition fname (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl @@ -630,7 +630,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof | _ -> assert false in let fixpoint_exprl = [fixpoint_expr] in - let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err "Function" (str "Body of Function must be given") in let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let using_lemmas = [] in let pre_hook pconstants = @@ -656,7 +656,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof let fixpoint_exprl = [fixpoint_expr] in let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let using_lemmas = [] in - let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in + let body = match body with | Some body -> body | None -> user_err "Function" (str "Body of Function must be given") in let pre_hook pconstants = generate_principle (ref (Evd.from_env (Global.env ()))) diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index ff1db8cf5..536c6ff4b 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -62,7 +62,7 @@ DECLARE PLUGIN "ssrmatching_plugin" type loc = Loc.t let dummy_loc = Loc.ghost let errorstrm = CErrors.errorlabstrm "ssrmatching" -let loc_error loc msg = CErrors.user_err_loc (loc, msg, str msg) +let loc_error loc msg = CErrors.user_err ~loc msg (str msg) let ppnl = Feedback.msg_info (* 0 cost pp function. Active only if env variable SSRDEBUG is set *) diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index e18d19ced..c6fe553c5 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -52,8 +52,8 @@ let interp_ascii_string dloc s = if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2] then int_of_string s else - user_err_loc (dloc,"interp_ascii_string", - str "Expects a single character or a three-digits ascii code.") in + user_err ~loc:dloc "interp_ascii_string" + (str "Expects a single character or a three-digits ascii code.") in interp_ascii dloc p let uninterp_ascii r = diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index a9eb126b4..6d62496ee 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -47,8 +47,8 @@ let nat_of_int dloc n = mk_nat ref_O n end else - user_err_loc (dloc, "nat_of_int", - str "Cannot interpret a negative number as a number of type nat") + user_err "nat_of_int" + (str "Cannot interpret a negative number as a number of type nat") (************************************************************************) (* Printing via scopes *) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index f65f9b791..ac28714f5 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -100,7 +100,7 @@ let int31_of_pos_bigint dloc n = GApp (dloc, ref_construct, List.rev (args 31 n)) let error_negative dloc = - CErrors.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.") + CErrors.user_err ~loc:dloc "interp_int31" (Pp.str "int31 are only non-negative numbers.") let interp_int31 dloc n = if is_pos_or_zero n then @@ -189,7 +189,7 @@ let bigN_of_pos_bigint dloc n = GApp (dloc, ref_constructor, args) let bigN_error_negative dloc = - CErrors.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.") + CErrors.user_err ~loc:dloc "interp_bigN" (Pp.str "bigN are only non-negative numbers.") let interp_bigN dloc n = if is_pos_or_zero n then diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 60803a369..851ea3b74 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -57,8 +57,8 @@ let pos_of_bignat dloc x = pos_of x let error_non_positive dloc = - user_err_loc (dloc, "interp_positive", - str "Only strictly positive numbers in type \"positive\".") + user_err ~loc:dloc "interp_positive" + (str "Only strictly positive numbers in type \"positive\".") let interp_positive dloc n = if is_strictly_pos n then pos_of_bignat dloc n @@ -113,7 +113,7 @@ let n_of_binnat dloc pos_or_neg n = GRef (dloc, glob_N0, None) let error_negative dloc = - user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".") + user_err ~loc:dloc "interp_N" (str "No negative numbers in type \"N\".") let n_of_int dloc n = if is_pos_or_zero n then n_of_binnat dloc true n diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 447a4c487..85c518019 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 ba566f374..6bc61f6dd 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 913e80f39..98dea9fc9 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 85125a502..ab9393915 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 0fea2ba22..26af90958 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 f9ab75cea..b91ae6c72 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 fe73b6105..99c3772db 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 00b6100c0..5b0958695 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 880f48e5f..73f81923f 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 1ef96e034..8b0bdb009 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 diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f71719cb9..a7742d866 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -700,7 +700,7 @@ let read_sec_context r = let dir = try Nametab.locate_section qid with Not_found -> - user_err_loc (loc,"read_sec_context", str "Unknown section.") in + user_err ~loc "read_sec_context" (str "Unknown section.") in let rec get_cxt in_cxt = function | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest -> if DirPath.equal dir dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 5f0cc73d2..ce216e563 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -54,8 +54,8 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc with e when CErrors.noncritical e -> let loc = Glob_ops.loc_of_glob_constr rawc in - user_err_loc - (loc,"", str "Instance is not well-typed in the environment of " ++ + user_err ~loc "" + (str "Instance is not well-typed in the environment of " ++ pr_existential_key sigma evk ++ str ".") in define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 7605f6387..7b43b64ef 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -202,8 +202,8 @@ let discard (loc,id) = let n = List.length !pstates in discard_gen id; if Int.equal (List.length !pstates) n then - CErrors.user_err_loc - (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ()) + CErrors.user_err ~loc + "Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ()) let discard_current () = if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates diff --git a/stm/lemmas.ml b/stm/lemmas.ml index fb2f0351d..4552ba8c6 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -222,7 +222,7 @@ let compute_proof_name locality = function if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) then - user_err_loc (loc,"",pr_id id ++ str " already exists."); + user_err ~loc "" (pr_id id ++ str " already exists."); id, pl | None -> next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None @@ -331,7 +331,7 @@ let get_proof proof do_guard hook opacity = let check_exist = List.iter (fun (loc,id) -> if not (Nametab.exists_cci (Lib.make_path id)) then - user_err_loc (loc,"",pr_id id ++ str " does not exist.") + user_err ~loc "" (pr_id id ++ str " does not exist.") ) let universe_proof_terminator compute_guard hook = diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 475005648..3257d406a 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -294,8 +294,8 @@ let find_applied_relation metas loc env sigma c left2right = match decompose_applied_relation metas env sigma c ctype left2right with | Some c -> c | None -> - user_err_loc (loc, "decompose_applied_relation", - str"The type" ++ spc () ++ Printer.pr_constr_env env sigma ctype ++ + user_err ~loc "decompose_applied_relation" + (str"The type" ++ spc () ++ Printer.pr_constr_env env sigma ctype ++ spc () ++ str"of this term does not end with an applied relation.") (* To add rewriting rules to a base *) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 87fdcf14d..28a7b634c 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -172,14 +172,14 @@ let check_or_and_pattern_size check_and loc names branchsigns = let n = Array.length branchsigns in let msg p1 p2 = strbrk "a conjunctive pattern made of " ++ int p1 ++ (if p1 == p2 then mt () else str " or " ++ int p2) ++ str " patterns" in let err1 p1 p2 = - user_err_loc (loc,"",str "Expects " ++ msg p1 p2 ++ str ".") in + user_err ~loc "" (str "Expects " ++ msg p1 p2 ++ str ".") in let errn n = - user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n + user_err ~loc "" (str "Expects a disjunctive pattern with " ++ int n ++ str " branches.") in let err1' p1 p2 = - user_err_loc (loc,"",strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in + user_err ~loc "" (strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in let errforthcoming loc = - user_err_loc (loc,"",strbrk "Unexpected non atomic pattern.") in + user_err ~loc "" (strbrk "Unexpected non atomic pattern.") in match names with | IntroAndPattern l -> if not (Int.equal n 1) then errn n; @@ -508,7 +508,7 @@ module New = struct | [] -> () | (evk,evi) :: _ -> let (loc,_) = evi.Evd.evar_source in - Pretype_errors.error_unsolvable_implicit loc env sigma evk None + Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None let tclWITHHOLES accept_unresolved_holes tac sigma = tclEVARMAP >>= fun sigma_initial -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 38af9a0ca..ef66e6146 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -423,7 +423,7 @@ let find_name mayrepl decl naming gl = match naming with let ids_of_hyps = Tacmach.New.pf_ids_of_hyps gl in let id' = next_ident_away id ids_of_hyps in if not mayrepl && not (Id.equal id' id) then - user_err_loc (loc,"",pr_id id ++ str" is already used."); + user_err ~loc "" (pr_id id ++ str" is already used."); id (**************************************************************) @@ -2235,7 +2235,7 @@ let error_unexpected_extra_pattern loc bound pat = | IntroNaming (IntroIdentifier _) -> "name", (String.plural nb " introduction pattern"), "no" | _ -> "introduction pattern", "", "none" in - user_err_loc (loc,"",str "Unexpected " ++ str s1 ++ str " (" ++ + user_err ~loc "" (str "Unexpected " ++ str s1 ++ str " (" ++ (if Int.equal nb 0 then (str s3 ++ str s2) else (str "at most " ++ int nb ++ str s2)) ++ spc () ++ str (if Int.equal nb 1 then "was" else "were") ++ @@ -2475,8 +2475,8 @@ and prepare_intros_loc loc with_evars dft destopt = function (fun _ l -> clear_wildcards l) in fun id -> intro_pattern_action loc with_evars true true ipat [] destopt tac id) - | IntroForthcoming _ -> user_err_loc - (loc,"",str "Introduction pattern for one hypothesis expected.") + | IntroForthcoming _ -> user_err ~loc "" + (str "Introduction pattern for one hypothesis expected.") let intro_patterns_bound_to with_evars n destopt = intro_patterns_core with_evars true [] [] [] destopt @@ -2643,7 +2643,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = | IntroFresh heq_base -> fresh_id_in_env [id] heq_base env | IntroIdentifier id -> if List.mem id (ids_of_named_context (named_context env)) then - user_err_loc (loc,"",pr_id id ++ str" is already used."); + user_err ~loc "" (pr_id id ++ str" is already used."); id in let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in @@ -4392,7 +4392,7 @@ let induction_gen_l isrec with_evars elim names lc = let lc = List.map (function | (c,None) -> c | (c,Some(loc,eqname)) -> - user_err_loc (loc,"",str "Do not know what to do with " ++ + user_err ~loc "" (str "Do not know what to do with " ++ Miscprint.pr_intro_pattern_naming eqname)) lc in let rec atomize_list l = match l with diff --git a/toplevel/classes.ml b/toplevel/classes.ml index d6a6162f9..26cb7451a 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -66,8 +66,8 @@ let existing_instance glob g pri = match class_of_constr r with | Some (_, ((tc,u), _)) -> add_instance (new_instance tc pri glob (*FIXME*) (Flags.use_polymorphic_flag ()) c) - | None -> user_err_loc (loc_of_reference g, "declare_instance", - Pp.str "Constant does not build instances of a declared type class.") + | None -> user_err ~loc:(loc_of_reference g) "declare_instance" + (Pp.str "Constant does not build instances of a declared type class.") let mismatched_params env n m = mismatched_ctx_inst env Parameters n m let mismatched_props env n m = mismatched_ctx_inst env Properties n m diff --git a/toplevel/command.ml b/toplevel/command.ml index 097865648..b9a72fa33 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -57,8 +57,8 @@ let rec complete_conclusion a cs = function | CHole (loc, k, _, _) -> let (has_no_args,name,params) = a in if not has_no_args then - user_err_loc (loc,"", - strbrk"Cannot infer the non constant arguments of the conclusion of " + user_err ~loc "" + (strbrk"Cannot infer the non constant arguments of the conclusion of " ++ pr_id cs ++ str "."); let args = List.map (fun id -> CRef(Ident(loc,id),None)) params in CAppExpl (loc,(None,Ident(loc,name),None),List.rev args) @@ -330,7 +330,7 @@ let do_assumptions kind nl l = match l with | (Discharge, _, _) when Lib.sections_are_opened () -> let loc = fst id in let msg = Pp.str "Section variables cannot be polymorphic." in - user_err_loc (loc, "", msg) + user_err ~loc "" msg | _ -> () in do_assumptions_bound_univs coe kind nl id (Some pl) c @@ -342,7 +342,7 @@ let do_assumptions kind nl l = match l with let loc = fst id in let msg = Pp.str "Assumptions with bound universes can only be defined one at a time." in - user_err_loc (loc, "", msg) + user_err ~loc "" msg in (coe, (List.map map idl, c)) in @@ -438,7 +438,7 @@ let interp_ind_arity env evdref ind = let t, impls = understand_tcc_evars env evdref ~expected_type:IsType c, imps in let pseudo_poly = check_anonymous_type c in let () = if not (Reduction.is_arity env t) then - user_err_loc (constr_loc ind.ind_arity, "", str "Not an arity") + user_err ~loc:(constr_loc ind.ind_arity) "" (str "Not an arity") in t, pseudo_poly, impls @@ -553,7 +553,7 @@ let check_named (loc, na) = match na with | Name _ -> () | Anonymous -> let msg = str "Parameters must be named." in - user_err_loc (loc, "", msg) + user_err ~loc "" msg let check_param = function @@ -954,9 +954,9 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let relty = Typing.unsafe_type_of env !evdref rel in let relargty = let error () = - user_err_loc (constr_loc r, - "Command.build_wellfounded", - Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.") + user_err ~loc:(constr_loc r) + "Command.build_wellfounded" + (Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.") in try let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 29d745732..38d4a62b4 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -34,7 +34,7 @@ let check_evars env evm = | Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_,_,false) -> () | _ -> - Pretype_errors.error_unsolvable_implicit loc env evm key None) + Pretype_errors.error_unsolvable_implicit ~loc env evm key None) (Evd.undefined_map evm) type oblinfo = @@ -985,7 +985,7 @@ and solve_obligation_by_tac prg obls i tac = let (e, _) = CErrors.push e in match e with | Refiner.FailError (_, s) -> - user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s) + user_err ~loc:(fst obl.obl_location) "solve_obligation" (Lazy.force s) | e -> None (* FIXME really ? *) and solve_prg_obligations prg ?oblset tac = diff --git a/toplevel/record.ml b/toplevel/record.ml index 71d070776..6a64b0d66 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -102,7 +102,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = let error bk (loc, name) = match bk, name with | Default _, Anonymous -> - user_err_loc (loc, "record", str "Record parameters must be named") + user_err ~loc "record" (str "Record parameters must be named") | _ -> () in List.iter @@ -127,7 +127,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = sred, true | None -> s, false else s, false) - | _ -> user_err_loc (constr_loc t,"", str"Sort expected.")) + | _ -> user_err ~loc:(constr_loc t) "" (str"Sort expected.")) | None -> let uvarkind = Evd.univ_flexible_alg in mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), true @@ -539,8 +539,8 @@ let declare_existing_class g = match g with | ConstRef x -> add_constant_class x | IndRef x -> add_inductive_class x - | _ -> user_err_loc (Loc.dummy_loc, "declare_existing_class", - Pp.str"Unsupported class type, only constants and inductives are allowed") + | _ -> user_err "declare_existing_class" + (Pp.str"Unsupported class type, only constants and inductives are allowed") open Vernacexpr diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index f83ada466..00655497b 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -70,7 +70,7 @@ let disable_drop = function | Drop -> CErrors.error "Drop is forbidden." | e -> e -let user_error loc s = CErrors.user_err_loc (loc,"_",str s) +let user_error loc s = CErrors.user_err ~loc "_" (str s) (* Opening and closing a channel. Open it twice when verbose: the first channel is used to read the commands, and the second one to print them. diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f69c4fa18..3f784fd8a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -380,9 +380,9 @@ let err_unmapped_library loc ?from qid = | Some from -> str " and prefix " ++ pr_dirpath from ++ str "." in - user_err_loc - (loc,"locate_library", - strbrk "Cannot find a physical path bound to logical path matching suffix " ++ + user_err ~loc + "locate_library" + (strbrk "Cannot find a physical path bound to logical path matching suffix " ++ pr_dirpath dir ++ prefix) let err_notfound_library loc ?from qid = @@ -391,9 +391,8 @@ let err_notfound_library loc ?from qid = | Some from -> str " with prefix " ++ pr_dirpath from ++ str "." in - user_err_loc - (loc,"locate_library", - strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) + user_err ~loc "locate_library" + (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) let print_located_library r = let (loc,qid) = qualid_of_reference r in @@ -605,15 +604,15 @@ let vernac_combined_scheme lid l = let vernac_universe loc poly l = if poly && not (Lib.sections_are_opened ()) then - user_err_loc (loc, "vernac_universe", - str"Polymorphic universes can only be declared inside sections, " ++ + user_err ~loc "vernac_universe" + (str"Polymorphic universes can only be declared inside sections, " ++ str "use Monomorphic Universe instead"); do_universe poly l let vernac_constraint loc poly l = if poly && not (Lib.sections_are_opened ()) then - user_err_loc (loc, "vernac_constraint", - str"Polymorphic universe constraints can only be declared" + user_err ~loc "vernac_constraint" + (str"Polymorphic universe constraints can only be declared" ++ str " inside sections, use Monomorphic Constraint instead"); do_constraint poly l @@ -1575,8 +1574,8 @@ let global_module r = let (loc,qid) = qualid_of_reference r in try Nametab.full_name_module qid with Not_found -> - user_err_loc (loc, "global_module", - str "Module/section " ++ pr_qualid qid ++ str " not found.") + user_err ~loc "global_module" + (str "Module/section " ++ pr_qualid qid ++ str " not found.") let interp_search_restriction = function | SearchOutside l -> (List.map global_module l, true) |