aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.mli8
-rw-r--r--interp/constrintern.ml24
-rw-r--r--interp/constrintern.mli11
-rw-r--r--interp/declare.ml8
-rw-r--r--interp/declare.mli4
-rw-r--r--interp/dumpglob.ml2
-rw-r--r--interp/dumpglob.mli8
-rw-r--r--interp/impargs.ml4
-rw-r--r--interp/impargs.mli9
-rw-r--r--interp/implicit_quantifiers.ml2
-rw-r--r--interp/implicit_quantifiers.mli7
-rw-r--r--interp/interp.mllib1
-rw-r--r--interp/notation.ml51
-rw-r--r--interp/notation.mli17
-rw-r--r--interp/notation_ops.ml12
-rw-r--r--interp/notation_term.ml123
-rw-r--r--interp/reserve.ml2
-rw-r--r--interp/smartlocate.mli8
-rw-r--r--interp/stdarg.mli7
19 files changed, 212 insertions, 96 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 8ab70283c8..73c108319f 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -13,13 +13,11 @@ open Termops
open EConstr
open Environ
open Libnames
-open Globnames
open Glob_term
open Pattern
open Constrexpr
open Notation_term
open Notation
-open Misctypes
open Ltac_pretype
(** Translation of pattern, cases pattern, glob_constr and term into syntax
@@ -40,7 +38,7 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob
val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr
val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
-val extern_reference : ?loc:Loc.t -> Id.Set.t -> global_reference -> reference
+val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference
val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort
val extern_rel_context : constr option -> env -> Evd.evar_map ->
@@ -58,9 +56,9 @@ val print_projections : bool ref
(** Customization of the global_reference printer *)
val set_extern_reference :
- (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) -> unit
+ (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference) -> unit
val get_extern_reference :
- unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference)
+ unit -> (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference)
(** WARNING: The following functions are evil due to
side-effects. Think of the following case as used in the printer:
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7eda89f4e1..48f15f8979 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -980,17 +980,17 @@ let intern_reference ref =
in
Smartlocate.global_of_extended_global r
-let sort_info_of_level_info (info: Misctypes.level_info) : (Libnames.reference * int) option =
+let sort_info_of_level_info (info: level_info) : (Libnames.reference * int) option =
match info with
- | Misctypes.UAnonymous -> None
- | Misctypes.UUnknown -> None
- | Misctypes.UNamed id -> Some (id, 0)
+ | UAnonymous -> None
+ | UUnknown -> None
+ | UNamed id -> Some (id, 0)
-let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort =
+let glob_sort_of_level (level: glob_level) : glob_sort =
match level with
- | Misctypes.GProp -> Misctypes.GProp
- | Misctypes.GSet -> Misctypes.GSet
- | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info]
+ | GProp -> GProp
+ | GSet -> GSet
+ | GType info -> GType [sort_info_of_level_info info]
(* Is it a global reference or a syntactic definition? *)
let intern_qualid qid intern env ntnvars us args =
@@ -1024,7 +1024,7 @@ let intern_qualid qid intern env ntnvars us args =
DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg)
| _ -> err ()
end
- | Some [s], GSort (Misctypes.GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
+ | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
| Some [_old_level], GSort _new_sort ->
(* TODO: add old_level and new_sort to the error message *)
user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid.v)
@@ -1077,7 +1077,7 @@ let interp_reference vars r =
(** Private internalization patterns *)
type 'a raw_cases_pattern_expr_r =
| RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname
- | RCPatCstr of Globnames.global_reference
+ | RCPatCstr of GlobRef.t
* 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list
(** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *)
| RCPatAtom of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
@@ -1314,7 +1314,7 @@ let sort_fields ~complete loc fields completer =
| [] -> (idx, acc_first_idx, acc)
| (Some field_glob_id) :: projs ->
let field_glob_ref = ConstRef field_glob_id in
- let first_field = eq_gr field_glob_ref first_field_glob_ref in
+ let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in
begin match proj_kinds with
| [] -> anomaly (Pp.str "Number of projections mismatch.")
| (_, regular) :: proj_kinds ->
@@ -1352,7 +1352,7 @@ let sort_fields ~complete loc fields completer =
user_err ?loc ~hdr:"intern"
(str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
let remaining_projs, (field_index, _) =
- let the_proj (idx, glob_id) = eq_gr field_glob_ref (ConstRef glob_id) in
+ let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in
try CList.extract_first the_proj remaining_projs
with Not_found ->
user_err ?loc
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index f5e32dc4cd..4dd719e1f3 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -13,7 +13,6 @@ open Evd
open Environ
open Misctypes
open Libnames
-open Globnames
open Glob_term
open Pattern
open EConstr
@@ -143,7 +142,7 @@ val intern_constr_pattern :
constr_pattern_expr -> patvar list * constr_pattern
(** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
-val intern_reference : reference -> global_reference
+val intern_reference : reference -> GlobRef.t
(** Expands abbreviations (syndef); raise an error if not existing *)
val interp_reference : ltac_sign -> reference -> glob_constr
@@ -175,11 +174,11 @@ val interp_context_evars :
(** Locating references of constructions, possibly via a syntactic definition
(these functions do not modify the glob file) *)
-val locate_reference : Libnames.qualid -> Globnames.global_reference
+val locate_reference : Libnames.qualid -> GlobRef.t
val is_global : Id.t -> bool
-val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> Globnames.global_reference
-val global_reference : Id.t -> Globnames.global_reference
-val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_reference
+val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> GlobRef.t
+val global_reference : Id.t -> GlobRef.t
+val global_reference_in_absolute_module : DirPath.t -> Id.t -> GlobRef.t
(** Interprets a term as the left-hand side of a notation. The returned map is
guaranteed to have the same domain as the input one. *)
diff --git a/interp/declare.ml b/interp/declare.ml
index c55a6c69ba..bc2d2068a2 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -487,7 +487,7 @@ let add_universe src (dp, i) =
Option.iter (fun poly ->
let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
Global.push_context_set poly ctx;
- Universes.add_global_universe level poly;
+ UnivNames.add_global_universe level poly;
if poly then Lib.add_section_context ctx)
optpoly
@@ -538,7 +538,7 @@ let input_universe : universe_decl -> Libobject.obj =
let declare_univ_binders gr pl =
if Global.is_polymorphic gr then
- Universes.register_universe_binders gr pl
+ UnivNames.register_universe_binders gr pl
else
let l = match gr with
| ConstRef c -> Label.to_id @@ Constant.label c
@@ -564,7 +564,7 @@ let do_universe poly l =
in
let l =
List.map (fun {CAst.v=id} ->
- let lev = Universes.new_univ_id () in
+ let lev = UnivGen.new_univ_id () in
(id, lev)) l
in
let src = if poly then BoundUniv else UnqualifiedUniv in
@@ -595,7 +595,7 @@ let input_constraints : constraint_decl -> Libobject.obj =
let do_constraint poly l =
let u_of_id x =
let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
- Universes.is_polymorphic level, level
+ UnivNames.is_polymorphic level, level
in
let in_section = Lib.sections_are_opened () in
let () =
diff --git a/interp/declare.mli b/interp/declare.mli
index 084d746e68..4a9f542783 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -83,10 +83,10 @@ val recursive_message : bool (** true = fixpoint *) ->
val exists_name : Id.t -> bool
(** Global universe contexts, names and constraints *)
-val declare_univ_binders : Globnames.global_reference -> Universes.universe_binders -> unit
+val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
val do_universe : polymorphic -> Misctypes.lident list -> unit
-val do_constraint : polymorphic -> (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list ->
+val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list ->
unit
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index bc6a1ef3aa..74618a2905 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -254,7 +254,7 @@ let dump_def ?loc ty secpath id = Option.iter (fun loc ->
let dump_definition {CAst.loc;v=id} sec s =
dump_def ?loc s (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id)
-let dump_constraint (({ CAst.loc; v = n },_), _, _) sec ty =
+let dump_constraint { CAst.loc; v = n } sec ty =
match n with
| Names.Name id -> dump_definition CAst.(make ?loc id) sec ty
| Names.Anonymous -> ()
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 43c100008c..bf83d2df40 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -24,7 +24,7 @@ val feedback_glob : unit -> unit
val pause : unit -> unit
val continue : unit -> unit
-val add_glob : ?loc:Loc.t -> Globnames.global_reference -> unit
+val add_glob : ?loc:Loc.t -> Names.GlobRef.t -> unit
val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit
val dump_definition : Misctypes.lident -> bool -> string -> unit
@@ -38,9 +38,9 @@ val dump_binding : ?loc:Loc.t -> Names.Id.Set.elt -> unit
val dump_notation :
(Constrexpr.notation * Notation.notation_location) Loc.located ->
Notation_term.scope_name option -> bool -> unit
-val dump_constraint :
- Vernacexpr.typeclass_constraint -> bool -> string -> unit
+
+val dump_constraint : Misctypes.lname -> bool -> string -> unit
val dump_string : string -> unit
-val type_of_global_ref : Globnames.global_reference -> string
+val type_of_global_ref : Names.GlobRef.t -> string
diff --git a/interp/impargs.ml b/interp/impargs.ml
index b424f73dea..7e4c4ef4f7 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -505,7 +505,7 @@ type implicit_discharge_request =
| ImplLocal
| ImplConstant of Constant.t * implicits_flags
| ImplMutualInductive of MutInd.t * implicits_flags
- | ImplInteractive of global_reference * implicits_flags *
+ | ImplInteractive of GlobRef.t * implicits_flags *
implicit_interactive_request
let implicits_table = Summary.ref Refmap.empty ~name:"implicits"
@@ -626,7 +626,7 @@ let classify_implicits (req,_ as obj) = match req with
type implicits_obj =
implicit_discharge_request *
- (global_reference * implicits_list list) list
+ (GlobRef.t * implicits_list list) list
let inImplicits : implicits_obj -> obj =
declare_object {(default_object "IMPLICITS") with
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 103a4f9e95..ea5aa90f68 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -10,7 +10,6 @@
open Names
open EConstr
-open Globnames
open Environ
(** {6 Implicit Arguments } *)
@@ -103,7 +102,7 @@ val declare_var_implicits : variable -> unit
val declare_constant_implicits : Constant.t -> unit
val declare_mib_implicits : MutInd.t -> unit
-val declare_implicits : bool -> global_reference -> unit
+val declare_implicits : bool -> GlobRef.t -> unit
(** [declare_manual_implicits local ref enriching l]
Manual declaration of which arguments are expected implicit.
@@ -111,15 +110,15 @@ val declare_implicits : bool -> global_reference -> unit
implicits depending on the current state.
Unsets implicits if [l] is empty. *)
-val declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
+val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
manual_implicits list -> unit
(** If the list is empty, do nothing, otherwise declare the implicits. *)
-val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
+val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
manual_implicits -> unit
-val implicits_of_global : global_reference -> implicits_list list
+val implicits_of_global : GlobRef.t -> implicits_list list
val extract_impargs_data :
implicits_list list -> ((int * int) option * implicit_status list) list
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 58df9abc4a..289890544f 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -58,7 +58,7 @@ let in_generalizable : bool * Misctypes.lident list option -> obj =
classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj)
}
-let declare_generalizable local gen =
+let declare_generalizable ~local gen =
Lib.add_anonymous_leaf (in_generalizable (local, gen))
let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index b9815f34d5..39d0174f99 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -12,9 +12,8 @@ open Names
open Glob_term
open Constrexpr
open Libnames
-open Globnames
-val declare_generalizable : Vernacexpr.locality_flag -> Misctypes.lident list option -> unit
+val declare_generalizable : local:bool -> Misctypes.lident list option -> unit
val ids_of_list : Id.t list -> Id.Set.t
val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t
@@ -39,10 +38,10 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
val combine_params_freevar :
- Id.Set.t -> global_reference option * Context.Rel.Declaration.t ->
+ Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t ->
Constrexpr.constr_expr * Id.Set.t
val implicit_application : Id.Set.t -> ?allow_partial:bool ->
- (Id.Set.t -> global_reference option * Context.Rel.Declaration.t ->
+ (Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t ->
Constrexpr.constr_expr * Id.Set.t) ->
constr_expr -> constr_expr * Id.Set.t
diff --git a/interp/interp.mllib b/interp/interp.mllib
index bb22cf468d..61313acc48 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,6 +1,7 @@
Tactypes
Stdarg
Genintern
+Notation_term
Notation_ops
Notation
Syntax_def
diff --git a/interp/notation.ml b/interp/notation.ml
index 47d6481350..e6df7b96c9 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -49,7 +49,6 @@ type notation_location = (DirPath.t * DirPath.t) * string
type notation_data = {
not_interp : interpretation;
not_location : notation_location;
- not_onlyprinting : bool;
}
type scope = {
@@ -259,7 +258,7 @@ type interp_rule =
according to the key of the pattern (adapted from Chet Murthy by HH) *)
type key =
- | RefKey of global_reference
+ | RefKey of GlobRef.t
| Oth
let key_compare k1 k2 = match k1, k2 with
@@ -430,13 +429,15 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
(* Uninterpreted notation levels *)
-let declare_notation_level ntn level =
+let declare_notation_level ?(onlyprint=false) ntn level =
if String.Map.mem ntn !notation_level_map then
anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level.");
- notation_level_map := String.Map.add ntn level !notation_level_map
+ notation_level_map := String.Map.add ntn (level,onlyprint) !notation_level_map
-let level_of_notation ntn =
- String.Map.find ntn !notation_level_map
+let level_of_notation ?(onlyprint=false) ntn =
+ let (level,onlyprint') = String.Map.find ntn !notation_level_map in
+ if onlyprint' && not onlyprint then raise Not_found;
+ level
(* The mapping between notations and their interpretation *)
@@ -449,20 +450,21 @@ let warn_notation_overridden =
let declare_notation_interpretation ntn scopt pat df ~onlyprint =
let scope = match scopt with Some s -> s | None -> default_scope in
let sc = find_scope scope in
- let () =
- if String.Map.mem ntn sc.notations then
- let which_scope = match scopt with
- | None -> mt ()
- | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in
- warn_notation_overridden (ntn,which_scope)
- in
- let notdata = {
- not_interp = pat;
- not_location = df;
- not_onlyprinting = onlyprint;
- } in
- let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in
- let () = scope_map := String.Map.add scope sc !scope_map in
+ if not onlyprint then begin
+ let () =
+ if String.Map.mem ntn sc.notations then
+ let which_scope = match scopt with
+ | None -> mt ()
+ | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in
+ warn_notation_overridden (ntn,which_scope)
+ in
+ let notdata = {
+ not_interp = pat;
+ not_location = df;
+ } in
+ let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in
+ scope_map := String.Map.add scope sc !scope_map
+ end;
begin match scopt with
| None -> scope_stack := SingleNotation ntn :: !scope_stack
| Some _ -> ()
@@ -487,7 +489,6 @@ let rec find_interpretation ntn find = function
let find_notation ntn sc =
let n = String.Map.find ntn (find_scope sc).notations in
- let () = if n.not_onlyprinting then raise Not_found in
(n.not_interp, n.not_location)
let notation_of_prim_token = function
@@ -631,7 +632,6 @@ let exists_notation_in_scope scopt ntn onlyprint r =
try
let sc = String.Map.find scope !scope_map in
let n = String.Map.find ntn sc.notations in
- onlyprint = n.not_onlyprinting &&
interpretation_eq n.not_interp r
with Not_found -> false
@@ -778,7 +778,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
(req,r,0,l1@l,cls1)
type arguments_scope_obj =
- arguments_scope_discharge_request * global_reference *
+ arguments_scope_discharge_request * GlobRef.t *
(* Used to communicate information from discharge to rebuild *)
(* set to 0 otherwise *) int *
scope_name option list * scope_class option list
@@ -1051,7 +1051,7 @@ let locate_notation prglob ntn scope =
| [] -> str "Unknown notation"
| _ ->
str "Notation" ++ fnl () ++
- prlist (fun (ntn,l) ->
+ prlist_with_sep fnl (fun (ntn,l) ->
let scope = find_default ntn scopes in
prlist
(fun (sc,r,(_,df)) ->
@@ -1060,8 +1060,7 @@ let locate_notation prglob ntn scope =
(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 ()))
+ then spc () ++ str "(default interpretation)" else mt ())))
l) ntns
let collect_notation_in_scope scope sc known =
diff --git a/interp/notation.mli b/interp/notation.mli
index 6803a7e517..ccc67fe491 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -11,7 +11,6 @@
open Bigint
open Names
open Libnames
-open Globnames
open Constrexpr
open Glob_term
open Notation_term
@@ -91,7 +90,7 @@ val declare_string_interpreter : scope_name -> required_module ->
val interp_prim_token : ?loc:Loc.t -> prim_token -> local_scopes ->
glob_constr * (notation_location * scope_name option)
(* This function returns a glob_const representing a pattern *)
-val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (global_reference -> unit) -> prim_token ->
+val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (GlobRef.t -> unit) -> prim_token ->
local_scopes -> glob_constr * (notation_location * scope_name option)
(** Return the primitive token associated to a [term]/[cases_pattern];
@@ -138,13 +137,13 @@ val availability_of_notation : scope_name option * notation -> local_scopes ->
(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
-val declare_notation_level : notation -> level -> unit
-val level_of_notation : notation -> level (** raise [Not_found] if no level *)
+val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit
+val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *)
(** {6 Miscellaneous} *)
-val interp_notation_as_global_reference : ?loc:Loc.t -> (global_reference -> bool) ->
- notation -> delimiters option -> global_reference
+val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) ->
+ notation -> delimiters option -> GlobRef.t
(** Checks for already existing notations *)
val exists_notation_in_scope : scope_name option -> notation ->
@@ -152,9 +151,9 @@ val exists_notation_in_scope : scope_name option -> notation ->
(** Declares and looks for scopes associated to arguments of a global ref *)
val declare_arguments_scope :
- bool (** true=local *) -> global_reference -> scope_name option list -> unit
+ bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit
-val find_arguments_scope : global_reference -> scope_name option list
+val find_arguments_scope : GlobRef.t -> scope_name option list
type scope_class
@@ -165,7 +164,7 @@ val subst_scope_class :
Mod_subst.substitution -> scope_class -> scope_class option
val declare_scope_class : scope_name -> scope_class -> unit
-val declare_ref_arguments_scope : Evd.evar_map -> global_reference -> unit
+val declare_ref_arguments_scope : Evd.evar_map -> GlobRef.t -> unit
val compute_arguments_scope : Evd.evar_map -> EConstr.types -> scope_name option list
val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index a76f820941..b806dce0b1 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -28,7 +28,7 @@ open Notation_term
let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None
let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
-| NRef gr1, NRef gr2 -> eq_gr gr1 gr2
+| NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2
| NVar id1, NVar id2 -> (
match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with
| Some n,Some m -> Int.equal n m
@@ -165,15 +165,15 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
| NApp (a,args) -> GApp (f e a, List.map (f e) args)
| NList (x,y,iter,tail,swap) ->
let t = f e tail in let it = f e iter in
- let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in
+ let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in
let inner = lt @@ GApp (lt @@ GVar (ldots_var),[subst_glob_vars innerl it]) in
- let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in
+ let outerl = (ldots_var,inner)::(if swap then [] else [y, lt @@ GVar x]) in
DAst.get (subst_glob_vars outerl it)
| NBinderList (x,y,iter,tail,swap) ->
let t = f e tail in let it = f e iter in
- let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in
+ let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in
let inner = lt @@ GApp (lt @@ GVar ldots_var,[subst_glob_vars innerl it]) in
- let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in
+ let outerl = (ldots_var,inner)::(if swap then [] else [y, lt @@ GVar x]) in
DAst.get (subst_glob_vars outerl it)
| NLambda (na,ty,c) ->
let e',disjpat,na = g e na in GLambda (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
@@ -1123,7 +1123,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
(* Matching compositionally *)
| GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
- | GRef (r1,_), NRef r2 when (eq_gr r1 r2) -> sigma
+ | GRef (r1,_), NRef r2 when (GlobRef.equal r1 r2) -> sigma
| GApp (f1,l1), NApp (f2,l2) ->
let n1 = List.length l1 and n2 = List.length l2 in
let f1,l1,f2,l2 =
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
new file mode 100644
index 0000000000..1a46746cc9
--- /dev/null
+++ b/interp/notation_term.ml
@@ -0,0 +1,123 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+open Misctypes
+open Glob_term
+
+(** [notation_constr] *)
+
+(** [notation_constr] is the subtype of [glob_constr] allowed in syntactic
+ extensions (i.e. notations).
+ No location since intended to be substituted at any place of a text.
+ Complex expressions such as fixpoints and cofixpoints are excluded,
+ as well as non global expressions such as existential variables. *)
+
+type notation_constr =
+ (** Part common to [glob_constr] and [cases_pattern] *)
+ | NRef of GlobRef.t
+ | NVar of Id.t
+ | NApp of notation_constr * notation_constr list
+ | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option
+ | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
+ (** Part only in [glob_constr] *)
+ | NLambda of Name.t * notation_constr * notation_constr
+ | NProd of Name.t * notation_constr * notation_constr
+ | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
+ | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr
+ | NCases of Constr.case_style * notation_constr option *
+ (notation_constr * (Name.t * (inductive * Name.t list) option)) list *
+ (cases_pattern list * notation_constr) list
+ | NLetTuple of Name.t list * (Name.t * notation_constr option) *
+ notation_constr * notation_constr
+ | NIf of notation_constr * (Name.t * notation_constr option) *
+ notation_constr * notation_constr
+ | NRec of fix_kind * Id.t array *
+ (Name.t * notation_constr option * notation_constr) list array *
+ notation_constr array * notation_constr array
+ | NSort of glob_sort
+ | NCast of notation_constr * notation_constr cast_type
+ | NProj of Projection.t * notation_constr
+
+(** Note concerning NList: first constr is iterator, second is terminator;
+ first id is where each argument of the list has to be substituted
+ in iterator and snd id is alternative name just for printing;
+ boolean is associativity *)
+
+(** Types concerning notations *)
+
+type scope_name = string
+
+type tmp_scope_name = scope_name
+
+type subscopes = tmp_scope_name option * scope_name list
+
+(** Type of the meta-variables of an notation_constr: in a recursive pattern x..y,
+ x carries the sequence of objects bound to the list x..y *)
+
+type notation_binder_source =
+ (* This accepts only pattern *)
+ (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *)
+ | NtnParsedAsPattern of bool
+ (* This accepts only ident *)
+ | NtnParsedAsIdent
+ (* This accepts ident, or pattern, or both *)
+ | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind
+
+type notation_var_instance_type =
+ | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList
+
+(** Type of variables when interpreting a constr_expr as a notation_constr:
+ in a recursive pattern x..y, both x and y carry the individual type
+ of each element of the list x..y *)
+type notation_var_internalization_type =
+ | NtnInternTypeAny | NtnInternTypeOnlyBinder
+
+(** This characterizes to what a notation is interpreted to *)
+type interpretation =
+ (Id.t * (subscopes * notation_var_instance_type)) list *
+ notation_constr
+
+type reversibility_status = APrioriReversible | HasLtac | NonInjective of Id.t list
+
+type notation_interp_env = {
+ ninterp_var_type : notation_var_internalization_type Id.Map.t;
+ ninterp_rec_vars : Id.t Id.Map.t;
+}
+
+type grammar_constr_prod_item =
+ | GramConstrTerminal of Tok.t
+ | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option
+ | GramConstrListMark of int * bool * int
+ (* tells action rule to make a list of the n previous parsed items;
+ concat with last parsed list when true; additionally release
+ the p last items as if they were parsed autonomously *)
+
+(** Dealing with precedences *)
+
+type precedence = int
+type parenRelation = L | E | Any | Prec of precedence
+type tolerability = precedence * parenRelation
+
+type level = precedence * tolerability list * Extend.constr_entry_key list
+
+(** Grammar rules for a notation *)
+
+type one_notation_grammar = {
+ notgram_level : level;
+ notgram_assoc : Extend.gram_assoc option;
+ notgram_notation : Constrexpr.notation;
+ notgram_prods : grammar_constr_prod_item list list;
+}
+
+type notation_grammar = {
+ notgram_onlyprinting : bool;
+ notgram_rules : one_notation_grammar list
+}
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 36005121b1..b57103cf22 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -22,7 +22,7 @@ open Notation_ops
open Globnames
type key =
- | RefKey of global_reference
+ | RefKey of GlobRef.t
| Oth
(** TODO: share code from Notation *)
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 7ff7e899e2..45037b8b36 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -18,22 +18,22 @@ open Misctypes
if not bound in the global env; raise a [UserError] if bound to a
syntactic def that does not denote a reference *)
-val locate_global_with_alias : ?head:bool -> qualid CAst.t -> global_reference
+val locate_global_with_alias : ?head:bool -> qualid CAst.t -> GlobRef.t
(** Extract a global_reference from a reference that can be an "alias" *)
-val global_of_extended_global : extended_global_reference -> global_reference
+val global_of_extended_global : extended_global_reference -> GlobRef.t
(** Locate a reference taking into account possible "alias" notations.
May raise [Nametab.GlobalizationError _] for an unknown reference,
or a [UserError] if bound to a syntactic def that does not denote
a reference. *)
-val global_with_alias : ?head:bool -> reference -> global_reference
+val global_with_alias : ?head:bool -> reference -> GlobRef.t
(** The same for inductive types *)
val global_inductive_with_alias : reference -> inductive
(** Locate a reference taking into account notations and "aliases" *)
-val smart_global : ?head:bool -> reference or_by_notation -> global_reference
+val smart_global : ?head:bool -> reference or_by_notation -> GlobRef.t
(** The same for inductive types *)
val smart_global_inductive : reference or_by_notation -> inductive
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 53d1a522d3..dc9c370a1b 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -14,7 +14,6 @@ open Loc
open Names
open EConstr
open Libnames
-open Globnames
open Genredexpr
open Pattern
open Constrexpr
@@ -42,7 +41,7 @@ val wit_ident : Id.t uniform_genarg_type
val wit_var : (lident, lident, Id.t) genarg_type
-val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
+val wit_ref : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
@@ -81,8 +80,8 @@ val wit_clause_dft_concl : (lident Locus.clause_expr, lident Locus.clause_expr,
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_reference : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
+val wit_global : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
val wit_clause : (lident Locus.clause_expr, lident 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 CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 11:35:20 +0000