aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrarg.ml74
-rw-r--r--interp/constrarg.mli87
-rw-r--r--interp/constrexpr_ops.ml16
-rw-r--r--interp/constrextern.ml4
-rw-r--r--interp/constrintern.ml159
-rw-r--r--interp/coqlib.ml2
-rw-r--r--interp/dumpglob.ml17
-rw-r--r--interp/genintern.ml18
-rw-r--r--interp/genintern.mli11
-rw-r--r--interp/implicit_quantifiers.ml24
-rw-r--r--interp/interp.mllib1
-rw-r--r--interp/modintern.ml8
-rw-r--r--interp/notation.ml49
-rw-r--r--interp/notation_ops.ml16
-rw-r--r--interp/ppextend.ml6
-rw-r--r--interp/ppextend.mli3
-rw-r--r--interp/reserve.ml8
-rw-r--r--interp/smartlocate.ml10
-rw-r--r--interp/stdarg.ml45
-rw-r--r--interp/stdarg.mli60
-rw-r--r--interp/syntax_def.ml2
-rw-r--r--interp/topconstr.ml10
-rw-r--r--interp/topconstr.mli2
23 files changed, 296 insertions, 336 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
deleted file mode 100644
index ca828102b9..0000000000
--- a/interp/constrarg.ml
+++ /dev/null
@@ -1,74 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Loc
-open Tacexpr
-open Misctypes
-open Genarg
-open Geninterp
-
-let make0 ?dyn name =
- let wit = Genarg.make0 name in
- let () = Geninterp.register_val0 wit dyn in
- wit
-
-(** This is a hack for now, to break the dependency of Genarg on constr-related
- types. We should use dedicated functions someday. *)
-
-let loc_of_or_by_notation f = function
- | AN c -> f c
- | ByNotation (loc,s,_) -> loc
-
-let wit_int_or_var =
- make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var"
-
-let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type =
- make0 "intropattern"
-
-let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
- make0 "tactic"
-
-let wit_ltac = make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac"
-
-let wit_ident =
- make0 "ident"
-
-let wit_var =
- make0 ~dyn:(val_tag (topwit wit_ident)) "var"
-
-let wit_ref = make0 "ref"
-
-let wit_quant_hyp = make0 "quant_hyp"
-
-let wit_constr =
- make0 "constr"
-
-let wit_uconstr = make0 "uconstr"
-
-let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
-
-let wit_constr_with_bindings = make0 "constr_with_bindings"
-
-let wit_bindings = make0 "bindings"
-
-let wit_red_expr = make0 "redexpr"
-
-let wit_clause_dft_concl =
- make0 "clause_dft_concl"
-
-let wit_destruction_arg =
- make0 "destruction_arg"
-
-(** Aliases *)
-
-let wit_reference = wit_ref
-let wit_global = wit_ref
-let wit_clause = wit_clause_dft_concl
-let wit_quantified_hypothesis = wit_quant_hyp
-let wit_intropattern = wit_intro_pattern
-let wit_redexpr = wit_red_expr
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
deleted file mode 100644
index 6ccd944d43..0000000000
--- a/interp/constrarg.mli
+++ /dev/null
@@ -1,87 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(** Generic arguments based on [constr]. We put them here to avoid a dependency
- of Genarg in [constr]-related interfaces. *)
-
-open Loc
-open Names
-open Term
-open Libnames
-open Globnames
-open Genredexpr
-open Pattern
-open Constrexpr
-open Tacexpr
-open Misctypes
-open Genarg
-
-(** FIXME: nothing to do there. *)
-val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
-
-(** {5 Additional generic arguments} *)
-
-val wit_int_or_var : (int or_var, int or_var, int) genarg_type
-
-val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
-
-val wit_ident : Id.t uniform_genarg_type
-
-val wit_var : (Id.t located, Id.t located, Id.t) genarg_type
-
-val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
-
-val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
-
-val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
-
-val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
-
-val wit_open_constr :
- (constr_expr, glob_constr_and_expr, constr) genarg_type
-
-val wit_constr_with_bindings :
- (constr_expr with_bindings,
- glob_constr_and_expr with_bindings,
- constr with_bindings delayed_open) genarg_type
-
-val wit_bindings :
- (constr_expr bindings,
- glob_constr_and_expr bindings,
- constr bindings delayed_open) genarg_type
-
-val wit_red_expr :
- ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
- (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
- (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
-
-val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_type
-
-(** [wit_ltac] is subtly different from [wit_tactic]: they only change for their
- toplevel interpretation. The one of [wit_ltac] forces the tactic and
- discards the result. *)
-val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type
-
-val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
-
-val wit_destruction_arg :
- (constr_expr with_bindings destruction_arg,
- glob_constr_and_expr with_bindings destruction_arg,
- delayed_open_constr_with_bindings destruction_arg) genarg_type
-
-(** Aliases for compatibility *)
-
-val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type
-val wit_global : (reference, global_reference located or_var, global_reference) genarg_type
-val wit_clause : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
-val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
-val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
-val wit_redexpr :
- ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
- (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
- (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 04429851fd..59c24900d2 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 ~hdr:"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)
+ ~hdr:"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) ~hdr:"coerce_to_name"
+ (str "This expression should be a name.")
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index dd8a48b85e..3077231be0 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) ~hdr:"encode_record"
+ (str "This type is not a structure type.");
indsp
module PrintingRecordRecord =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c916fcd886..3ed8733df5 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 ~hdr:"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:
@@ -366,19 +366,19 @@ let check_hidden_implicit_parameters id impls =
| (Inductive indparams,_,_,_) -> Id.List.mem id indparams
| _ -> false) impls
then
- errorlabstrm "" (strbrk "A parameter of an inductive type " ++
+ user_err (strbrk "A parameter of an inductive type " ++
pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
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;
@@ -660,23 +660,13 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
let arg = match arg with
| None -> None
| Some arg ->
- let open Tacexpr in
- let open Genarg in
- let wit = glbwit Constrarg.wit_tactic in
- let body =
- if has_type arg wit then out_gen wit arg
- else assert false (** FIXME *)
- in
- let mk_env id (c, (tmp_scope, subscopes)) accu =
+ let mk_env (c, (tmp_scope, subscopes)) =
let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
let gc = intern nenv c in
- let c = ConstrMayEval (Genredexpr.ConstrTerm (gc, Some c)) in
- ((loc, id), c) :: accu
+ (gc, Some c)
in
- let bindings = Id.Map.fold mk_env terms [] in
- let tac = TacLetIn (false, bindings, body) in
- let arg = in_gen wit tac in
- Some arg
+ let bindings = Id.Map.map mk_env terms in
+ Some (Genintern.generic_substitute_notation bindings arg)
in
GHole (loc, knd, naming, arg)
| NBinderList (x,y,iter,terminator) ->
@@ -764,7 +754,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 +778,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 ~hdr:"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 +815,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 +824,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 +837,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 +862,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 +878,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 +894,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 +972,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 +981,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 +1006,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 +1024,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 +1032,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 ~hdr:"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 ~hdr:"find_constructor" error
in
cstr, match add_params with
| Some nb_args ->
@@ -1067,7 +1057,7 @@ let check_duplicate loc fields =
match dups with
| [] -> ()
| (r, _) :: _ ->
- user_err_loc (loc, "", str "This record defines several times the field " ++
+ user_err ~loc (str "This record defines several times the field " ++
pr_reference r ++ str ".")
(** [sort_fields ~complete loc fields completer] expects a list
@@ -1092,8 +1082,8 @@ let sort_fields ~complete loc fields completer =
let gr = global_reference_of_reference first_field_ref in
(gr, Recordops.find_projection gr)
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) ~hdr:"intern"
+ (pr_reference first_field_ref ++ str": Not a projection")
in
(* the number of parameters *)
let nparams = record.Recordops.s_EXPECTEDPARAM in
@@ -1123,7 +1113,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
@@ -1136,7 +1126,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
@@ -1150,15 +1140,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) ~hdr:"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)
| [] ->
@@ -1229,7 +1218,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
@@ -1354,8 +1343,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
@@ -1370,7 +1359,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 =
@@ -1422,8 +1411,8 @@ let rec intern_pat genv aliases pat =
[pattern] rule. *)
let rec check_no_patcast = function
| CPatCast (loc,_,_) ->
- CErrors.user_err_loc (loc, "check_no_patcast",
- Pp.strbrk "Casts are not supported here.")
+ CErrors.user_err ~loc ~hdr:"check_no_patcast"
+ (Pp.strbrk "Casts are not supported here.")
| CPatDelimiters(_,_,p)
| CPatAlias(_,p,_) -> check_no_patcast p
| CPatCstr(_,_,opl,pl) ->
@@ -1456,11 +1445,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
@@ -1468,8 +1457,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 *)
@@ -1508,10 +1497,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) ->
@@ -1521,11 +1510,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)
@@ -1576,7 +1565,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 ->
@@ -1603,7 +1592,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
(fun ((loc,id),bl,ty,_) ->
let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in
let rbl = List.map (function BDRawDef a -> a | BDPattern _ ->
- Loc.raise loc (Stream.Error "pattern with quote not allowed after cofix")) rbl in
+ Loc.raise ~loc (Stream.Error "pattern with quote not allowed after cofix")) rbl in
(List.rev rbl,
intern_type env' ty,env')) dl in
let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') ->
@@ -1681,7 +1670,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 ~hdr:"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
@@ -1751,7 +1740,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let k = match k with
| None ->
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
- Evar_kinds.QuestionMark st
+ (match naming with
+ | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id
+ | _ -> Evar_kinds.QuestionMark st)
| Some k -> k
in
let solve = match solve with
@@ -1904,7 +1895,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"."));
[]
@@ -1935,8 +1926,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 ~hdr:"internalize"
+ (explain_internalization_error e)
(**************************************************************************)
(* Functions to translate constr_expr into glob_constr *)
@@ -1975,7 +1966,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 ~hdr:"internalize" (explain_internalization_error e)
(*********************************************************************)
@@ -2086,13 +2077,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 ~hdr:"internalize" (explain_internalization_error e)
let interp_rawcontext_evars env evdref k bl =
let (env, par, _, impls) =
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 588637b76e..9539980f04 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -86,7 +86,7 @@ let check_required_library d =
(Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m)
*)
(* or failing ...*)
- errorlabstrm "Coqlib.check_required_library"
+ user_err ~hdr:"Coqlib.check_required_library"
(str "Library " ++ pr_dirpath dir ++ str " has to be required first.")
(************************************************************************)
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index b020f89457..9f549b0c0f 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -173,32 +173,33 @@ let cook_notation df sc =
(* - all single quotes in terminal tokens are doubled *)
(* - characters < 32 are represented by '^A, '^B, '^C, etc *)
(* The output is decoded in function Index.prepare_entry of coqdoc *)
- let ntn = String.make (String.length df * 5) '_' in
+ let ntn = Bytes.make (String.length df * 5) '_' in
let j = ref 0 in
let l = String.length df - 1 in
let i = ref 0 in
+ let open Bytes in (* Bytes.set *)
while !i <= l do
assert (df.[!i] != ' ');
if df.[!i] == '_' && (Int.equal !i l || df.[!i+1] == ' ') then
(* Next token is a non-terminal *)
- (ntn.[!j] <- 'x'; incr j; incr i)
+ (set ntn !j 'x'; incr j; incr i)
else begin
(* Next token is a terminal *)
- ntn.[!j] <- '\''; incr j;
+ set ntn !j '\''; incr j;
while !i <= l && df.[!i] != ' ' do
if df.[!i] < ' ' then
let c = char_of_int (int_of_char 'A' + int_of_char df.[!i] - 1) in
(String.blit ("'^" ^ String.make 1 c) 0 ntn !j 3; j := !j+3; incr i)
else begin
- if df.[!i] == '\'' then (ntn.[!j] <- '\''; incr j);
- ntn.[!j] <- df.[!i]; incr j; incr i
+ if df.[!i] == '\'' then (set ntn !j '\''; incr j);
+ set ntn !j df.[!i]; incr j; incr i
end
done;
- ntn.[!j] <- '\''; incr j
+ set ntn !j '\''; incr j
end;
- if !i <= l then (ntn.[!j] <- '_'; incr j; incr i)
+ if !i <= l then (set ntn !j '_'; incr j; incr i)
done;
- let df = String.sub ntn 0 !j in
+ let df = Bytes.sub_string ntn 0 !j in
match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df
let dump_notation_location posl df (((path,secpath),_),sc) =
diff --git a/interp/genintern.ml b/interp/genintern.ml
index d6bfd347ff..be7abfa995 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -16,6 +16,7 @@ type glob_sign = {
type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
type 'glb subst_fun = substitution -> 'glb -> 'glb
+type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
module InternObj =
struct
@@ -31,8 +32,16 @@ struct
let default _ = None
end
+module NtnSubstObj =
+struct
+ type ('raw, 'glb, 'top) obj = 'glb ntn_subst_fun
+ let name = "notation_subst"
+ let default _ = None
+end
+
module Intern = Register (InternObj)
module Subst = Register (SubstObj)
+module NtnSubst = Register (NtnSubstObj)
let intern = Intern.obj
let register_intern0 = Intern.register0
@@ -50,3 +59,12 @@ let generic_substitute subs (GenArg (Glbwit wit, v)) =
in_gen (glbwit wit) (substitute wit subs v)
let () = Hook.set Detyping.subst_genarg_hook generic_substitute
+
+(** Notation substitution *)
+
+let substitute_notation = NtnSubst.obj
+let register_ntn_subst0 = NtnSubst.register0
+
+let generic_substitute_notation env (GenArg (Glbwit wit, v)) =
+ let v = substitute_notation wit env v in
+ in_gen (glbwit wit) v
diff --git a/interp/genintern.mli b/interp/genintern.mli
index 4b244b38d8..4b0354be39 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -32,6 +32,14 @@ val substitute : ('raw, 'glb, 'top) genarg_type -> 'glb subst_fun
val generic_substitute : glob_generic_argument subst_fun
+(** {5 Notation functions} *)
+
+type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
+
+val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun
+
+val generic_substitute_notation : glob_generic_argument ntn_subst_fun
+
(** Registering functions *)
val register_intern0 : ('raw, 'glb, 'top) genarg_type ->
@@ -39,3 +47,6 @@ val register_intern0 : ('raw, 'glb, 'top) genarg_type ->
val register_subst0 : ('raw, 'glb, 'top) genarg_type ->
'glb subst_fun -> unit
+
+val register_ntn_subst0 : ('raw, 'glb, 'top) genarg_type ->
+ 'glb ntn_subst_fun -> unit
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 10cfbe58fa..77a8ed680a 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -21,18 +21,20 @@ open Libobject
open Nameops
open Misctypes
open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
(*i*)
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 ~hdr:"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 ~hdr:"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 +80,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 ~hdr:"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 =
@@ -186,7 +188,7 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
vars
let rec make_fresh ids env x =
- if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_subscript x)
+ if is_freevar ids env x then x else make_fresh ids env (Nameops.increment_subscript x)
let next_name_away_from na avoid =
match na with
@@ -198,12 +200,12 @@ let combine_params avoid fn applied needed =
List.partition
(function
(t, Some (loc, ExplByName id)) ->
- let is_id (_, decl) = match get_name decl with
+ let is_id (_, decl) = match RelDecl.get_name decl with
| Name id' -> Id.equal id id'
| 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,12 +239,12 @@ 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 =
fun avoid (_, decl) ->
- let id' = next_name_away_from (get_name decl) avoid in
+ let id' = next_name_away_from (RelDecl.get_name decl) avoid in
(CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid)
let destClassApp cl =
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 96b52959a0..607af82a03 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,5 +1,4 @@
Stdarg
-Constrarg
Genintern
Constrexpr_ops
Notation_ops
diff --git a/interp/modintern.ml b/interp/modintern.ml
index e5dce5ccf3..d4ade7058a 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 389a1c9dff..66d3c91859 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -20,6 +20,9 @@ open Notation_term
open Glob_term
open Glob_ops
open Ppextend
+open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
(*i*)
(*s A scope is a set of notations; it includes
@@ -95,7 +98,7 @@ let declare_scope scope =
scope_map := String.Map.add scope empty_scope !scope_map
let error_unknown_scope sc =
- errorlabstrm "Notation"
+ user_err ~hdr:"Notation"
(str "Scope " ++ str sc ++ str " is not declared.")
let find_scope scope =
@@ -208,7 +211,7 @@ let remove_delimiters scope =
let sc = find_scope scope in
let newsc = { sc with delimiters = None } in
match sc.delimiters with
- | None -> CErrors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".")
+ | None -> CErrors.user_err (str "No bound key for scope " ++ str scope ++ str ".")
| Some key ->
scope_map := String.Map.add scope newsc !scope_map;
try
@@ -220,8 +223,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 ~hdr:"find_delimiters"
+ (str "Unknown scope delimiting key " ++ str key ++ str ".")
(* Uninterpretation tables *)
@@ -337,8 +340,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 ~hdr:"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 +461,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 ~hdr:"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 +486,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)
@@ -684,7 +687,7 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) =
let n =
try
let vars = Lib.variable_section_segment_of_reference r in
- List.length (List.filter (fun (_,_,b,_) -> b = None) vars)
+ vars |> List.map fst |> List.filter is_local_assum |> List.length
with
Not_found (* Not a ref defined in this section *) -> 0 in
Some (req,Lib.discharge_global r,n,l,[])
@@ -888,11 +891,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 =
@@ -924,19 +927,19 @@ let locate_notation prglob ntn scope =
match ntns with
| [] -> str "Unknown notation"
| _ ->
- t (str "Notation " ++
- tab () ++ str "Scope " ++ tab () ++ fnl () ++
+ str "Notation" ++ fnl () ++
prlist (fun (ntn,l) ->
let scope = find_default ntn scopes in
prlist
(fun (sc,r,(_,df)) ->
hov 0 (
- pr_notation_info prglob df r ++ tbrk (1,2) ++
- (if String.equal sc default_scope then mt () else (str ": " ++ str sc)) ++
- tbrk (1,2) ++
- (if Option.equal String.equal (Some sc) scope then str "(default interpretation)" else mt ())
+ pr_notation_info prglob df r ++
+ (if String.equal sc default_scope then mt ()
+ else (spc () ++ str ": " ++ str sc)) ++
+ (if Option.equal String.equal (Some sc) scope
+ then spc () ++ str "(default interpretation)" else mt ())
++ fnl ()))
- l) ntns)
+ l) ntns
let collect_notation_in_scope scope sc known =
assert (not (String.equal scope default_scope));
@@ -1018,8 +1021,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 ~hdr:"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 0c5393cf41..7dbd94aa74 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -242,8 +242,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'
@@ -294,8 +294,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,RecursiveTerms lassoc) ->
let newfound,x,y,lassoc =
if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) ||
@@ -338,8 +338,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
@@ -394,7 +394,7 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) =
let vars = Id.Map.filter filter nenv.ninterp_var_type in
let check_recvar x =
if Id.List.mem x found then
- errorlabstrm "" (pr_id x ++
+ user_err (pr_id x ++
strbrk " should only be used in the recursive part of a pattern.") in
let check (x, y) = check_recvar x; check_recvar y in
let () = List.iter check foundrec in
@@ -413,7 +413,7 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) =
in
let check_pair s x y where =
if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then
- errorlabstrm "" (strbrk "in the right-hand side, " ++ pr_id x ++
+ user_err (strbrk "in the right-hand side, " ++ pr_id x ++
str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++
str " position as part of a recursive pattern.") in
let check_type x typ =
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 37bbe0ce87..87ca253253 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -23,12 +23,9 @@ type ppbox =
| PpHOVB of int
| PpHVB of int
| PpVB of int
- | PpTB
type ppcut =
| PpBrk of int * int
- | PpTbrk of int * int
- | PpTab
| PpFnl
let ppcmd_of_box = function
@@ -36,13 +33,10 @@ let ppcmd_of_box = function
| PpHOVB n -> hov n
| PpHVB n -> hv n
| PpVB n -> v n
- | PpTB -> t
let ppcmd_of_cut = function
- | PpTab -> tab ()
| PpFnl -> fnl ()
| PpBrk(n1,n2) -> brk(n1,n2)
- | PpTbrk(n1,n2) -> tbrk(n1,n2)
type unparsing =
| UnpMetaVar of int * parenRelation
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index de7a42eee5..09dc369437 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -23,12 +23,9 @@ type ppbox =
| PpHOVB of int
| PpHVB of int
| PpVB of int
- | PpTB
type ppcut =
| PpBrk of int * int
- | PpTbrk of int * int
- | PpTab
| PpFnl
val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 388ca08050..a4d4f40277 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 ~hdr:"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 ~hdr:"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 478774219e..178c1c1f96 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) ~hdr:"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/stdarg.ml b/interp/stdarg.ml
index 2a7d52e3af..341ff5662c 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -6,6 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Loc
+open Misctypes
+open Tactypes
open Genarg
open Geninterp
@@ -29,7 +32,49 @@ let wit_string : string uniform_genarg_type =
let wit_pre_ident : string uniform_genarg_type =
make0 ~dyn:(val_tag (topwit wit_string)) "preident"
+let loc_of_or_by_notation f = function
+ | AN c -> f c
+ | ByNotation (loc,s,_) -> loc
+
+let wit_int_or_var =
+ make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var"
+
+let wit_intro_pattern =
+ make0 "intropattern"
+
+let wit_ident =
+ make0 "ident"
+
+let wit_var =
+ make0 ~dyn:(val_tag (topwit wit_ident)) "var"
+
+let wit_ref = make0 "ref"
+
+let wit_quant_hyp = make0 "quant_hyp"
+
+let wit_constr =
+ make0 "constr"
+
+let wit_uconstr = make0 "uconstr"
+
+let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
+
+let wit_constr_with_bindings = make0 "constr_with_bindings"
+
+let wit_bindings = make0 "bindings"
+
+let wit_red_expr = make0 "redexpr"
+
+let wit_clause_dft_concl =
+ make0 "clause_dft_concl"
+
(** Aliases for compatibility *)
let wit_integer = wit_int
let wit_preident = wit_pre_ident
+let wit_reference = wit_ref
+let wit_global = wit_ref
+let wit_clause = wit_clause_dft_concl
+let wit_quantified_hypothesis = wit_quant_hyp
+let wit_intropattern = wit_intro_pattern
+let wit_redexpr = wit_red_expr
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index e1f648d7fc..af3a734627 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -8,8 +8,21 @@
(** Basic generic arguments. *)
+open Loc
+open Names
+open Term
+open Libnames
+open Globnames
+open Genredexpr
+open Pattern
+open Constrexpr
+open Misctypes
+open Tactypes
open Genarg
+(** FIXME: nothing to do there. *)
+val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
+
val wit_unit : unit uniform_genarg_type
val wit_bool : bool uniform_genarg_type
@@ -20,7 +33,54 @@ val wit_string : string uniform_genarg_type
val wit_pre_ident : string uniform_genarg_type
+(** {5 Additional generic arguments} *)
+
+val wit_int_or_var : (int or_var, int or_var, int) genarg_type
+
+val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
+
+val wit_ident : Id.t uniform_genarg_type
+
+val wit_var : (Id.t located, Id.t located, Id.t) genarg_type
+
+val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
+
+val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
+
+val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
+
+val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
+
+val wit_open_constr :
+ (constr_expr, glob_constr_and_expr, constr) genarg_type
+
+val wit_constr_with_bindings :
+ (constr_expr with_bindings,
+ glob_constr_and_expr with_bindings,
+ constr with_bindings delayed_open) genarg_type
+
+val wit_bindings :
+ (constr_expr bindings,
+ glob_constr_and_expr bindings,
+ constr bindings delayed_open) genarg_type
+
+val wit_red_expr :
+ ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
+ (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
+ (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
+
+val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+
(** Aliases for compatibility *)
val wit_integer : int uniform_genarg_type
val wit_preident : string uniform_genarg_type
+val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type
+val wit_global : (reference, global_reference located or_var, global_reference) genarg_type
+val wit_clause : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
+val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
+val wit_redexpr :
+ ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
+ (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
+ (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 2523063e64..c3f4c4f302 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -30,7 +30,7 @@ let add_syntax_constant kn c onlyparse =
let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
if Nametab.exists_cci sp then
- errorlabstrm "cache_syntax_constant"
+ user_err ~hdr:"cache_syntax_constant"
(pr_id (basename sp) ++ str " already exists");
add_syntax_constant kn pat onlyparse;
Nametab.push_syndef (Nametab.Until i) sp kn
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a397ca82eb..fd57b70ca9 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -31,8 +31,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 *)
@@ -177,10 +177,10 @@ let split_at_annot bl na =
end
| LocalRawDef _ as x :: rest -> aux (x :: acc) rest
| LocalPattern (loc,_,_) :: rest ->
- Loc.raise loc (Stream.Error "pattern with quote not allowed after fix")
+ Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")
| [] ->
- 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 58edd4ddf8..95d702f8d5 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 -> unit -> 'a
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 03:59:33 +0000