diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-14 22:36:47 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-04 22:29:03 +0200 |
| commit | afceace455a4b37ced7e29175ca3424996195f7b (patch) | |
| tree | a76a6acc9e3210720d0920c4341a798eecdd3f18 | |
| parent | af19d08003173718c0f7c070d0021ad958fbe58d (diff) | |
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.
This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.
A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
129 files changed, 620 insertions, 625 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 2bad21bb2..6d7c0d368 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -4,7 +4,7 @@ Proof engine - More functions have been changed to use `EConstr`, notably the +- More functions have been changed to use `EConstr`, notably the functions in `Evd`, and in particular `Evd.define`. Note that the core function `EConstr.to_constr` now _enforces_ by @@ -18,6 +18,10 @@ Proof engine that setting this flag to false is deprecated so it is only meant to be used as to help port pre-EConstr code. +- A few type alias have been deprecated, in all cases the message + should indicate what the canonical form is. An important change is + the move of `Globnames.global_reference` to `Names.GlobRef.t`. + ## Changes between Coq 8.7 and Coq 8.8 ### Bug tracker @@ -94,6 +98,11 @@ Declaration of printers for arguments used only in vernac command happen. An alternative is to register the corresponding argument as a value, using "Geninterp.register_val0 wit None". +Types Alias deprecation and type relocation. + +- A few type alias have been deprecated, in all cases the message + should indicate what the canonical form is. + ### STM API The STM API has seen a general overhaul. The main change is the diff --git a/dev/top_printers.mli b/dev/top_printers.mli index dad6dcc1c..c23ba964c 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -87,7 +87,7 @@ val ppclosedglobconstr : Ltac_pretype.closed_glob_constr -> unit val ppclosedglobconstridmap : Ltac_pretype.closed_glob_constr Names.Id.Map.t -> unit -val ppglobal : Globnames.global_reference -> unit +val ppglobal : Names.GlobRef.t -> unit val ppconst : Names.KerName.t * (Constr.constr, 'a) Environ.punsafe_judgment -> unit diff --git a/engine/eConstr.ml b/engine/eConstr.ml index a72bdee12..d30cb74d7 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -500,6 +500,7 @@ let eq_universes env sigma cstrs cv_pb ref nargs l l' = let l = Evd.normalize_universe_instance sigma l and l' = Evd.normalize_universe_instance sigma l' in let open Universes in + let open GlobRef in match ref with | VarRef _ -> assert false (* variables don't have instances *) | ConstRef _ -> diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 9a5b5ec3a..743888a9b 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -284,9 +284,9 @@ val map_rel_context_in_env : (* XXX Missing Sigma proxy *) val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> - Evd.evar_map -> Globnames.global_reference -> Evd.evar_map * t + Evd.evar_map -> GlobRef.t -> Evd.evar_map * t -val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool +val is_global : Evd.evar_map -> GlobRef.t -> t -> bool (** {5 Extra} *) diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml index c964ecf1f..6e123d642 100644 --- a/engine/evar_kinds.ml +++ b/engine/evar_kinds.ml @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Globnames open Misctypes (** The kinds of existential variable *) @@ -24,7 +23,7 @@ type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patva type subevar_kind = Domain | Codomain | Body type t = - | ImplicitArg of global_reference * (int * Id.t option) + | ImplicitArg of GlobRef.t * (int * Id.t option) * bool (** Force inference *) | BinderType of Name.t | NamedHole of Id.t (* coming from some ?[id] syntax *) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 710491f84..6c27d5937 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -534,7 +534,7 @@ type clear_dependency_error = | OccurHypInSimpleClause of Id.t option | EvarTypingBreak of existential -exception ClearDependencyError of Id.t * clear_dependency_error * Globnames.global_reference option +exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option exception Depends of Id.t diff --git a/engine/evarutil.mli b/engine/evarutil.mli index e3e8f16c8..3bbd2923c 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -78,8 +78,8 @@ val restrict_evar : evar_map -> Evar.t -> Filter.t -> (** Polymorphic constants *) -val new_global : evar_map -> Globnames.global_reference -> evar_map * constr -val e_new_global : evar_map ref -> Globnames.global_reference -> constr +val new_global : evar_map -> GlobRef.t -> evar_map * constr +val e_new_global : evar_map ref -> GlobRef.t -> constr (** Create a fresh evar in a context different from its definition context: [new_evar_instance sign evd ty inst] creates a new evar of context @@ -235,7 +235,7 @@ type clear_dependency_error = | OccurHypInSimpleClause of Id.t option | EvarTypingBreak of Constr.existential -exception ClearDependencyError of Id.t * clear_dependency_error * Globnames.global_reference option +exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> Id.Set.t -> named_context_val * types diff --git a/engine/evd.mli b/engine/evd.mli index 5ce16459c..509db525d 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -649,7 +649,7 @@ val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> eva val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> - evar_map -> Globnames.global_reference -> evar_map * econstr + evar_map -> GlobRef.t -> evar_map * econstr (********************************************************************) (* constr with holes and pending resolution of classes, conversion *) diff --git a/engine/termops.mli b/engine/termops.mli index 3b0c4bba6..e2ddcd36e 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -112,7 +112,7 @@ val dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> bool val count_occurrences : Evd.evar_map -> constr -> constr -> int val collect_metas : Evd.evar_map -> constr -> int list val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *) -val vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t +val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t val occur_term : Evd.evar_map -> constr -> constr -> bool (** Synonymous of dependent *) [@@ocaml.deprecated "alias of Termops.dependent"] @@ -261,7 +261,7 @@ val clear_named_body : Id.t -> env -> env val global_vars : env -> Evd.evar_map -> constr -> Id.t list val global_vars_set : env -> Evd.evar_map -> constr -> Id.Set.t val global_vars_set_of_decl : env -> Evd.evar_map -> named_declaration -> Id.Set.t -val global_app_of_constr : Evd.evar_map -> constr -> (Globnames.global_reference * EInstance.t) * constr option +val global_app_of_constr : Evd.evar_map -> constr -> (GlobRef.t * EInstance.t) * constr option (** Gives an ordered list of hypotheses, closed by dependencies, containing a given set *) @@ -270,9 +270,9 @@ val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id. (** Test if an identifier is the basename of a global reference *) val is_section_variable : Id.t -> bool -val global_of_constr : Evd.evar_map -> constr -> Globnames.global_reference * EInstance.t +val global_of_constr : Evd.evar_map -> constr -> GlobRef.t * EInstance.t -val is_global : Evd.evar_map -> Globnames.global_reference -> constr -> bool +val is_global : Evd.evar_map -> GlobRef.t -> constr -> bool val isGlobalRef : Evd.evar_map -> constr -> bool diff --git a/engine/universes.ml b/engine/universes.ml index 0410d1aea..938f5ad9c 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -74,7 +74,7 @@ let subst_ubinder (subst,(ref,l as orig)) = let discharge_ubinder (_,(ref,l)) = Some (Lib.discharge_global ref, l) -let ubinder_obj : Globnames.global_reference * universe_binders -> Libobject.obj = +let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj = let open Libobject in declare_object { (default_object "universe binder") with cache_function = cache_ubinder; diff --git a/engine/universes.mli b/engine/universes.mli index a0a7749f8..e6bee42bb 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -37,8 +37,8 @@ type universe_binders = Univ.Level.t Names.Id.Map.t val empty_binders : universe_binders -val register_universe_binders : Globnames.global_reference -> universe_binders -> unit -val universe_binders_of_global : Globnames.global_reference -> universe_binders +val register_universe_binders : GlobRef.t -> universe_binders -> unit +val universe_binders_of_global : GlobRef.t -> universe_binders type univ_name_list = Misctypes.lname list @@ -48,7 +48,7 @@ type univ_name_list = Misctypes.lname list May error if the lengths mismatch. Otherwise return [universe_binders_of_global ref]. *) -val universe_binders_with_opt_names : Globnames.global_reference -> +val universe_binders_with_opt_names : Names.GlobRef.t -> Univ.Level.t list -> univ_name_list option -> universe_binders (** The global universe counter *) @@ -132,7 +132,7 @@ val fresh_inductive_instance : env -> inductive -> val fresh_constructor_instance : env -> constructor -> pconstructor in_universe_context_set -val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_reference -> +val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t -> constr in_universe_context_set val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> @@ -144,9 +144,9 @@ val fresh_universe_context_set_instance : ContextSet.t -> universe_level_subst * ContextSet.t (** Raises [Not_found] if not a global reference. *) -val global_of_constr : constr -> Globnames.global_reference puniverses +val global_of_constr : constr -> GlobRef.t puniverses -val constr_of_global_univ : Globnames.global_reference puniverses -> constr +val constr_of_global_univ : GlobRef.t puniverses -> constr val extend_context : 'a in_universe_context_set -> ContextSet.t -> 'a in_universe_context_set @@ -204,16 +204,16 @@ val normalize_universe_subst : universe_subst ref -> the constraints should be properly added to an evd. See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for the proper way to get a fresh copy of a global reference. *) -val constr_of_global : Globnames.global_reference -> constr +val constr_of_global : GlobRef.t -> constr (** ** DEPRECATED ** synonym of [constr_of_global] *) -val constr_of_reference : Globnames.global_reference -> constr +val constr_of_reference : GlobRef.t -> constr [@@ocaml.deprecated "synonym of [constr_of_global]"] (** Returns the type of the global reference, by creating a fresh instance of polymorphic references and computing their instantiated universe context. (side-effect on the universe counter, use with care). *) -val type_of_global : Globnames.global_reference -> types in_universe_context_set +val type_of_global : GlobRef.t -> types in_universe_context_set (** Full universes substitutions into terms *) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 8ab70283c..6f5887ca2 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -13,7 +13,6 @@ open Termops open EConstr open Environ open Libnames -open Globnames open Glob_term open Pattern open Constrexpr @@ -40,7 +39,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 +57,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 7eda89f4e..def8425ec 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -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 f5e32dc4c..4dd719e1f 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.mli b/interp/declare.mli index 084d746e6..f8cffbb1e 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -83,7 +83,7 @@ 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 -> Universes.universe_binders -> unit val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 43c100008..8dfb4f8f7 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 @@ -43,4 +43,4 @@ val dump_constraint : 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 b424f73de..7e4c4ef4f 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 103a4f9e9..ea5aa90f6 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.mli b/interp/implicit_quantifiers.mli index b9815f34d..5f4129ae0 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -12,7 +12,6 @@ open Names open Glob_term open Constrexpr open Libnames -open Globnames val declare_generalizable : Vernacexpr.locality_flag -> Misctypes.lident list option -> unit @@ -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/notation.ml b/interp/notation.ml index 47d648135..4a6d2a154 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -259,7 +259,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 @@ -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 diff --git a/interp/notation.mli b/interp/notation.mli index 6803a7e51..eac87414f 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]; @@ -143,8 +142,8 @@ val level_of_notation : notation -> level (** raise [Not_found] if no level *) (** {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 a76f82094..6a282624e 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 @@ -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 index a9c2e2a53..1a46746cc 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Globnames open Misctypes open Glob_term @@ -23,7 +22,7 @@ open Glob_term type notation_constr = (** Part common to [glob_constr] and [cases_pattern] *) - | NRef of global_reference + | 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 diff --git a/interp/reserve.ml b/interp/reserve.ml index 36005121b..b57103cf2 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 7ff7e899e..45037b8b3 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 53d1a522d..dc9c370a1 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 diff --git a/kernel/constr.ml b/kernel/constr.ml index 4f062d72f..bc486210d 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -654,7 +654,7 @@ let map_with_binders g f l c0 = match kind c0 with let bl' = CArray.Fun1.smartmap f l' bl in mkCoFix (ln,(lna,tl',bl')) -type instance_compare_fn = global_reference -> int -> +type instance_compare_fn = GlobRef.t -> int -> Univ.Instance.t -> Univ.Instance.t -> bool type constr_compare_fn = int -> constr -> constr -> bool @@ -692,10 +692,10 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal (eq 0) l1 l2 | Const (c1,u1), Const (c2,u2) -> (* The args length currently isn't used but may as well pass it. *) - Constant.equal c1 c2 && leq_universes (ConstRef c1) nargs u1 u2 - | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (IndRef c1) nargs u1 u2 + Constant.equal c1 c2 && leq_universes (GlobRef.ConstRef c1) nargs u1 u2 + | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (GlobRef.IndRef c1) nargs u1 u2 | Construct (c1,u1), Construct (c2,u2) -> - eq_constructor c1 c2 && leq_universes (ConstructRef c1) nargs u1 u2 + eq_constructor c1 c2 && leq_universes (GlobRef.ConstructRef c1) nargs u1 u2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> eq 0 p1 p2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2 | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> diff --git a/kernel/constr.mli b/kernel/constr.mli index 0d464840c..b35ea6653 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -413,7 +413,7 @@ val compare_head : constr_compare_fn -> constr_compare_fn (** Convert a global reference applied to 2 instances. The int says how many arguments are given (as we can only use cumulativity for fully applied inductives/constructors) .*) -type instance_compare_fn = global_reference -> int -> +type instance_compare_fn = GlobRef.t -> int -> Univ.Instance.t -> Univ.Instance.t -> bool (** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to diff --git a/kernel/names.ml b/kernel/names.ml index a3aa71f24..58d311dd5 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -701,22 +701,6 @@ end module Constrmap = Map.Make(ConstructorOrdered) module Constrmap_env = Map.Make(ConstructorOrdered_env) -type global_reference = - | VarRef of variable (** A reference to the section-context. *) - | ConstRef of Constant.t (** A reference to the environment. *) - | IndRef of inductive (** A reference to an inductive type. *) - | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) - -(* Better to have it here that in closure, since used in grammar.cma *) -type evaluable_global_reference = - | EvalVarRef of Id.t - | EvalConstRef of Constant.t - -let eq_egr e1 e2 = match e1, e2 with - EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2 - | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 - | _, _ -> false - (** {6 Hash-consing of name objects } *) module Hind = Hashcons.Make( @@ -904,6 +888,34 @@ end type projection = Projection.t +module GlobRef = struct + + type t = + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of Constant.t (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) + + let equal gr1 gr2 = + gr1 == gr2 || match gr1,gr2 with + | ConstRef con1, ConstRef con2 -> Constant.equal con1 con2 + | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2 + | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2 + | VarRef v1, VarRef v2 -> Id.equal v1 v2 + | (ConstRef _ | IndRef _ | ConstructRef _ | VarRef _), _ -> false + +end + +type evaluable_global_reference = + | EvalVarRef of Id.t + | EvalConstRef of Constant.t + +(* Better to have it here that in closure, since used in grammar.cma *) +let eq_egr e1 e2 = match e1, e2 with + EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2 + | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 + | _, _ -> false + let constant_of_kn = Constant.make1 let constant_of_kn_equiv = Constant.make let make_con = Constant.make3 diff --git a/kernel/names.mli b/kernel/names.mli index 96e020aed..566fcd0f9 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -500,21 +500,6 @@ val constructor_user_hash : constructor -> int val constructor_syntactic_ord : constructor -> constructor -> int val constructor_syntactic_hash : constructor -> int -(** {6 Global reference is a kernel side type for all references together } *) -type global_reference = - | VarRef of variable (** A reference to the section-context. *) - | ConstRef of Constant.t (** A reference to the environment. *) - | IndRef of inductive (** A reference to an inductive type. *) - | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) - -(** Better to have it here that in Closure, since required in grammar.cma *) -type evaluable_global_reference = - | EvalVarRef of Id.t - | EvalConstRef of Constant.t - -val eq_egr : evaluable_global_reference -> evaluable_global_reference - -> bool - (** {6 Hash-consing } *) val hcons_con : Constant.t -> Constant.t @@ -749,6 +734,29 @@ end type projection = Projection.t [@@ocaml.deprecated "Alias for [Projection.t]"] +(** {6 Global reference is a kernel side type for all references together } *) + +(* XXX: Should we define GlobRefCan GlobRefUser? *) +module GlobRef : sig + + type t = + | VarRef of variable (** A reference to the section-context. *) + | ConstRef of Constant.t (** A reference to the environment. *) + | IndRef of inductive (** A reference to an inductive type. *) + | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) + + val equal : t -> t -> bool + +end + +(** Better to have it here that in Closure, since required in grammar.cma *) +(* XXX: Move to a module *) +type evaluable_global_reference = + | EvalVarRef of Id.t + | EvalConstRef of Constant.t + +val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool + val constant_of_kn_equiv : KerName.t -> KerName.t -> Constant.t [@@ocaml.deprecated "Same as [Constant.make]"] diff --git a/library/coqlib.ml b/library/coqlib.ml index 3f01c617c..408e25919 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -171,16 +171,16 @@ let jmeq_kn = make_ind jmeq_module "JMeq" let glob_jmeq = IndRef (jmeq_kn,0) type coq_sigma_data = { - proj1 : global_reference; - proj2 : global_reference; - elim : global_reference; - intro : global_reference; - typ : global_reference } + proj1 : GlobRef.t; + proj2 : GlobRef.t; + elim : GlobRef.t; + intro : GlobRef.t; + typ : GlobRef.t } type coq_bool_data = { - andb : global_reference; - andb_prop : global_reference; - andb_true_intro : global_reference} + andb : GlobRef.t; + andb_prop : GlobRef.t; + andb_true_intro : GlobRef.t} let build_bool_type () = { andb = init_reference ["Datatypes"] "andb"; @@ -213,18 +213,18 @@ let build_prod () = (* Equalities *) type coq_eq_data = { - eq : global_reference; - ind : global_reference; - refl : global_reference; - sym : global_reference; - trans: global_reference; - congr: global_reference } + eq : GlobRef.t; + ind : GlobRef.t; + refl : GlobRef.t; + sym : GlobRef.t; + trans: GlobRef.t; + congr: GlobRef.t } (* Data needed for discriminate and injection *) type coq_inversion_data = { - inv_eq : global_reference; (* : forall params, t -> Prop *) - inv_ind : global_reference; (* : forall params P y, eq params y -> P y *) - inv_congr: global_reference (* : forall params B (f:t->B) y, eq params y -> f c=f y *) + inv_eq : GlobRef.t; (* : forall params, t -> Prop *) + inv_ind : GlobRef.t; (* : forall params P y, eq params y -> P y *) + inv_congr: GlobRef.t (* : forall params B (f:t->B) y, eq params y -> f c=f y *) } let lazy_init_reference dir id = lazy (init_reference dir id) diff --git a/library/coqlib.mli b/library/coqlib.mli index 8077c47c7..b4bd1b0e0 100644 --- a/library/coqlib.mli +++ b/library/coqlib.mli @@ -8,10 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Util open Names open Libnames -open Globnames -open Util (** This module collects the global references, constructions and patterns of the standard library used in ocaml files *) @@ -44,14 +43,14 @@ open Util type message = string -val find_reference : message -> string list -> string -> global_reference -val coq_reference : message -> string list -> string -> global_reference +val find_reference : message -> string list -> string -> GlobRef.t +val coq_reference : message -> string list -> string -> GlobRef.t (** For tactics/commands requiring vernacular libraries *) val check_required_library : string list -> unit (** Search in several modules (not prefixed by "Coq") *) -val gen_reference_in_modules : string->string list list-> string -> global_reference +val gen_reference_in_modules : string->string list list-> string -> GlobRef.t val arith_modules : string list list val zarith_base_modules : string list list @@ -78,24 +77,24 @@ val type_of_id : Constant.t (** Natural numbers *) val nat_path : full_path -val glob_nat : global_reference +val glob_nat : GlobRef.t val path_of_O : constructor val path_of_S : constructor -val glob_O : global_reference -val glob_S : global_reference +val glob_O : GlobRef.t +val glob_S : GlobRef.t (** Booleans *) -val glob_bool : global_reference +val glob_bool : GlobRef.t val path_of_true : constructor val path_of_false : constructor -val glob_true : global_reference -val glob_false : global_reference +val glob_true : GlobRef.t +val glob_false : GlobRef.t (** Equality *) -val glob_eq : global_reference -val glob_identity : global_reference -val glob_jmeq : global_reference +val glob_eq : GlobRef.t +val glob_identity : GlobRef.t +val glob_jmeq : GlobRef.t (** {6 ... } *) (** Constructions and patterns related to Coq initial state are unknown @@ -106,18 +105,18 @@ val glob_jmeq : global_reference at runtime. *) type coq_bool_data = { - andb : global_reference; - andb_prop : global_reference; - andb_true_intro : global_reference} + andb : GlobRef.t; + andb_prop : GlobRef.t; + andb_true_intro : GlobRef.t} val build_bool_type : coq_bool_data delayed (** {6 For Equality tactics } *) type coq_sigma_data = { - proj1 : global_reference; - proj2 : global_reference; - elim : global_reference; - intro : global_reference; - typ : global_reference } + proj1 : GlobRef.t; + proj2 : GlobRef.t; + elim : GlobRef.t; + intro : GlobRef.t; + typ : GlobRef.t } val build_sigma_set : coq_sigma_data delayed val build_sigma_type : coq_sigma_data delayed @@ -132,30 +131,30 @@ val build_sigma : coq_sigma_data delayed val build_prod : coq_sigma_data delayed type coq_eq_data = { - eq : global_reference; - ind : global_reference; - refl : global_reference; - sym : global_reference; - trans: global_reference; - congr: global_reference } + eq : GlobRef.t; + ind : GlobRef.t; + refl : GlobRef.t; + sym : GlobRef.t; + trans: GlobRef.t; + congr: GlobRef.t } val build_coq_eq_data : coq_eq_data delayed val build_coq_identity_data : coq_eq_data delayed val build_coq_jmeq_data : coq_eq_data delayed -val build_coq_eq : global_reference delayed (** = [(build_coq_eq_data()).eq] *) -val build_coq_eq_refl : global_reference delayed (** = [(build_coq_eq_data()).refl] *) -val build_coq_eq_sym : global_reference delayed (** = [(build_coq_eq_data()).sym] *) -val build_coq_f_equal2 : global_reference delayed +val build_coq_eq : GlobRef.t delayed (** = [(build_coq_eq_data()).eq] *) +val build_coq_eq_refl : GlobRef.t delayed (** = [(build_coq_eq_data()).refl] *) +val build_coq_eq_sym : GlobRef.t delayed (** = [(build_coq_eq_data()).sym] *) +val build_coq_f_equal2 : GlobRef.t delayed (** Data needed for discriminate and injection *) type coq_inversion_data = { - inv_eq : global_reference; (** : forall params, args -> Prop *) - inv_ind : global_reference; (** : forall params P (H : P params) args, eq params args + inv_eq : GlobRef.t; (** : forall params, args -> Prop *) + inv_ind : GlobRef.t; (** : forall params P (H : P params) args, eq params args -> P args *) - inv_congr: global_reference (** : forall params B (f:t->B) args, eq params args -> + inv_congr: GlobRef.t (** : forall params B (f:t->B) args, eq params args -> f params = f args *) } @@ -165,45 +164,45 @@ val build_coq_inversion_jmeq_data : coq_inversion_data delayed val build_coq_inversion_eq_true_data : coq_inversion_data delayed (** Specif *) -val build_coq_sumbool : global_reference delayed +val build_coq_sumbool : GlobRef.t delayed (** {6 ... } *) (** Connectives The False proposition *) -val build_coq_False : global_reference delayed +val build_coq_False : GlobRef.t delayed (** The True proposition and its unique proof *) -val build_coq_True : global_reference delayed -val build_coq_I : global_reference delayed +val build_coq_True : GlobRef.t delayed +val build_coq_I : GlobRef.t delayed (** Negation *) -val build_coq_not : global_reference delayed +val build_coq_not : GlobRef.t delayed (** Conjunction *) -val build_coq_and : global_reference delayed -val build_coq_conj : global_reference delayed -val build_coq_iff : global_reference delayed +val build_coq_and : GlobRef.t delayed +val build_coq_conj : GlobRef.t delayed +val build_coq_iff : GlobRef.t delayed -val build_coq_iff_left_proj : global_reference delayed -val build_coq_iff_right_proj : global_reference delayed +val build_coq_iff_left_proj : GlobRef.t delayed +val build_coq_iff_right_proj : GlobRef.t delayed (** Disjunction *) -val build_coq_or : global_reference delayed +val build_coq_or : GlobRef.t delayed (** Existential quantifier *) -val build_coq_ex : global_reference delayed - -val coq_eq_ref : global_reference lazy_t -val coq_identity_ref : global_reference lazy_t -val coq_jmeq_ref : global_reference lazy_t -val coq_eq_true_ref : global_reference lazy_t -val coq_existS_ref : global_reference lazy_t -val coq_existT_ref : global_reference lazy_t -val coq_exist_ref : global_reference lazy_t -val coq_not_ref : global_reference lazy_t -val coq_False_ref : global_reference lazy_t -val coq_sumbool_ref : global_reference lazy_t -val coq_sig_ref : global_reference lazy_t - -val coq_or_ref : global_reference lazy_t -val coq_iff_ref : global_reference lazy_t +val build_coq_ex : GlobRef.t delayed + +val coq_eq_ref : GlobRef.t lazy_t +val coq_identity_ref : GlobRef.t lazy_t +val coq_jmeq_ref : GlobRef.t lazy_t +val coq_eq_true_ref : GlobRef.t lazy_t +val coq_existS_ref : GlobRef.t lazy_t +val coq_existT_ref : GlobRef.t lazy_t +val coq_exist_ref : GlobRef.t lazy_t +val coq_not_ref : GlobRef.t lazy_t +val coq_False_ref : GlobRef.t lazy_t +val coq_sumbool_ref : GlobRef.t lazy_t +val coq_sig_ref : GlobRef.t lazy_t + +val coq_or_ref : GlobRef.t lazy_t +val coq_iff_ref : GlobRef.t lazy_t diff --git a/library/global.mli b/library/global.mli index 015f4d582..906d246ee 100644 --- a/library/global.mli +++ b/library/global.mli @@ -123,26 +123,26 @@ val env_of_context : Environ.named_context_val -> Environ.env val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit val is_joined_environment : unit -> bool -val is_polymorphic : Globnames.global_reference -> bool -val is_template_polymorphic : Globnames.global_reference -> bool -val is_type_in_type : Globnames.global_reference -> bool +val is_polymorphic : GlobRef.t -> bool +val is_template_polymorphic : GlobRef.t -> bool +val is_type_in_type : GlobRef.t -> bool val constr_of_global_in_context : Environ.env -> - Globnames.global_reference -> Constr.types * Univ.AUContext.t + GlobRef.t -> Constr.types * Univ.AUContext.t (** Returns the type of the constant in its local universe context. The type should not be used without pushing it's universe context in the environmnent of usage. For non-universe-polymorphic constants, it does not matter. *) val type_of_global_in_context : Environ.env -> - Globnames.global_reference -> Constr.types * Univ.AUContext.t + GlobRef.t -> Constr.types * Univ.AUContext.t (** Returns the type of the constant in its local universe context. The type should not be used without pushing it's universe context in the environmnent of usage. For non-universe-polymorphic constants, it does not matter. *) (** Returns the universe context of the global reference (whatever its polymorphic status is). *) -val universes_of_global : Globnames.global_reference -> Univ.AUContext.t +val universes_of_global : GlobRef.t -> Univ.AUContext.t (** {6 Retroknowledge } *) diff --git a/library/globnames.ml b/library/globnames.ml index 2fa3adba2..6b78d12ba 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -15,7 +15,7 @@ open Mod_subst open Libnames (*s Global reference is a kernel side type for all references together *) -type global_reference = Names.global_reference = +type global_reference = GlobRef.t = | VarRef of variable (** A reference to the section-context. *) | ConstRef of Constant.t (** A reference to the environment. *) | IndRef of inductive (** A reference to an inductive type. *) @@ -26,14 +26,6 @@ let isConstRef = function ConstRef _ -> true | _ -> false let isIndRef = function IndRef _ -> true | _ -> false let isConstructRef = function ConstructRef _ -> true | _ -> false -let eq_gr gr1 gr2 = - gr1 == gr2 || match gr1,gr2 with - | ConstRef con1, ConstRef con2 -> Constant.equal con1 con2 - | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2 - | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2 - | VarRef v1, VarRef v2 -> Id.equal v1 v2 - | (ConstRef _ | IndRef _ | ConstructRef _ | VarRef _), _ -> false - let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef" let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef" let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" @@ -245,3 +237,6 @@ let pop_global_reference = function | IndRef (kn,i) -> IndRef (pop_kn kn,i) | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j) | VarRef id -> anomaly (Pp.str "VarRef not poppable.") + +(* Deprecated *) +let eq_gr = GlobRef.equal diff --git a/library/globnames.mli b/library/globnames.mli index f2b88b870..2fe35ebcc 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -14,71 +14,73 @@ open Constr open Mod_subst (** {6 Global reference is a kernel side type for all references together } *) -type global_reference = Names.global_reference = +type global_reference = GlobRef.t = | VarRef of variable (** A reference to the section-context. *) | ConstRef of Constant.t (** A reference to the environment. *) | IndRef of inductive (** A reference to an inductive type. *) | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) +[@@ocaml.deprecated "Use Names.GlobRef.t"] -val isVarRef : global_reference -> bool -val isConstRef : global_reference -> bool -val isIndRef : global_reference -> bool -val isConstructRef : global_reference -> bool +val isVarRef : GlobRef.t -> bool +val isConstRef : GlobRef.t -> bool +val isIndRef : GlobRef.t -> bool +val isConstructRef : GlobRef.t -> bool -val eq_gr : global_reference -> global_reference -> bool -val canonical_gr : global_reference -> global_reference +val eq_gr : GlobRef.t -> GlobRef.t -> bool +[@@ocaml.deprecated "Use Names.GlobRef.equal"] +val canonical_gr : GlobRef.t -> GlobRef.t -val destVarRef : global_reference -> variable -val destConstRef : global_reference -> Constant.t -val destIndRef : global_reference -> inductive -val destConstructRef : global_reference -> constructor +val destVarRef : GlobRef.t -> variable +val destConstRef : GlobRef.t -> Constant.t +val destIndRef : GlobRef.t -> inductive +val destConstructRef : GlobRef.t -> constructor -val is_global : global_reference -> constr -> bool +val is_global : GlobRef.t -> constr -> bool val subst_constructor : substitution -> constructor -> constructor * constr -val subst_global : substitution -> global_reference -> global_reference * constr -val subst_global_reference : substitution -> global_reference -> global_reference +val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr +val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t (** This constr is not safe to be typechecked, universe polymorphism is not handled here: just use for printing *) -val printable_constr_of_global : global_reference -> constr +val printable_constr_of_global : GlobRef.t -> constr (** Turn a construction denoting a global reference into a global reference; raise [Not_found] if not a global reference *) -val global_of_constr : constr -> global_reference +val global_of_constr : constr -> GlobRef.t (** Obsolete synonyms for constr_of_global and global_of_constr *) -val reference_of_constr : constr -> global_reference +val reference_of_constr : constr -> GlobRef.t [@@ocaml.deprecated "Alias of Globnames.global_of_constr"] module RefOrdered : sig - type t = global_reference + type t = GlobRef.t val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> int end module RefOrdered_env : sig - type t = global_reference + type t = GlobRef.t val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> int end -module Refset : CSig.SetS with type elt = global_reference +module Refset : CSig.SetS with type elt = GlobRef.t module Refmap : Map.ExtS - with type key = global_reference and module Set := Refset + with type key = GlobRef.t and module Set := Refset -module Refset_env : CSig.SetS with type elt = global_reference +module Refset_env : CSig.SetS with type elt = GlobRef.t module Refmap_env : Map.ExtS - with type key = global_reference and module Set := Refset_env + with type key = GlobRef.t and module Set := Refset_env (** {6 Extended global references } *) type syndef_name = KerName.t type extended_global_reference = - | TrueGlobal of global_reference + | TrueGlobal of GlobRef.t | SynDef of syndef_name module ExtRefOrdered : sig @@ -89,7 +91,7 @@ module ExtRefOrdered : sig end type global_reference_or_constr = - | IsGlobal of global_reference + | IsGlobal of GlobRef.t | IsConstr of constr (** {6 Temporary function to brutally form kernel names from section paths } *) @@ -100,7 +102,6 @@ val encode_con : DirPath.t -> Id.t -> Constant.t val decode_con : Constant.t -> DirPath.t * Id.t (** {6 Popping one level of section in global names } *) - val pop_con : Constant.t -> Constant.t val pop_kn : MutInd.t-> MutInd.t -val pop_global_reference : global_reference -> global_reference +val pop_global_reference : GlobRef.t -> GlobRef.t diff --git a/library/keys.ml b/library/keys.ml index 34a6adabe..89363455d 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -10,12 +10,13 @@ (** Keys for unification and indexing *) -open Globnames +open Names open Term +open Globnames open Libobject type key = - | KGlob of global_reference + | KGlob of GlobRef.t | KLam | KLet | KProd @@ -126,7 +127,7 @@ let constr_key kind c = | Construct (c,u) -> KGlob (ConstructRef c) | Var id -> KGlob (VarRef id) | App (f, _) -> aux f - | Proj (p, _) -> KGlob (ConstRef (Names.Projection.constant p)) + | Proj (p, _) -> KGlob (ConstRef (Projection.constant p)) | Cast (p, _, _) -> aux p | Lambda _ -> KLam | Prod _ -> KProd diff --git a/library/keys.mli b/library/keys.mli index 1fb9a3de0..198383650 100644 --- a/library/keys.mli +++ b/library/keys.mli @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Globnames - type key val declare_equiv_keys : key -> key -> unit @@ -21,5 +19,5 @@ val equiv_keys : key -> key -> bool val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option (** Compute the head key of a term. *) -val pr_keys : (global_reference -> Pp.t) -> Pp.t +val pr_keys : (Names.GlobRef.t -> Pp.t) -> Pp.t (** Pretty-print the mapping *) diff --git a/library/lib.mli b/library/lib.mli index 26f1718cc..1d77212e9 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) - +open Names (** Lib: record of operations, backtrack, low-level sections *) (** This module provides a general mechanism to keep a trace of all operations @@ -28,7 +28,7 @@ type node = and library_segment = (Libnames.object_name * node) list -type lib_objects = (Names.Id.t * Libobject.obj) list +type lib_objects = (Id.t * Libobject.obj) list (** {6 Object iteration functions. } *) @@ -54,13 +54,13 @@ val segment_of_objects : (** Adding operations (which call the [cache] method, and getting the current list of operations (most recent ones coming first). *) -val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name +val add_leaf : Id.t -> Libobject.obj -> Libnames.object_name val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit val pull_to_head : Libnames.object_name -> unit (** this operation adds all objects with the same name and calls [load_object] for each of them *) -val add_leaves : Names.Id.t -> Libobject.obj list -> Libnames.object_name +val add_leaves : Id.t -> Libobject.obj list -> Libnames.object_name (** {6 ... } *) @@ -76,15 +76,15 @@ val contents_after : Libnames.object_name -> library_segment (** {6 Functions relative to current path } *) (** User-side names *) -val cwd : unit -> Names.DirPath.t -val cwd_except_section : unit -> Names.DirPath.t -val current_dirpath : bool -> Names.DirPath.t (* false = except sections *) -val make_path : Names.Id.t -> Libnames.full_path -val make_path_except_section : Names.Id.t -> Libnames.full_path +val cwd : unit -> DirPath.t +val cwd_except_section : unit -> DirPath.t +val current_dirpath : bool -> DirPath.t (* false = except sections *) +val make_path : Id.t -> Libnames.full_path +val make_path_except_section : Id.t -> Libnames.full_path (** Kernel-side names *) -val current_mp : unit -> Names.ModPath.t -val make_kn : Names.Id.t -> Names.KerName.t +val current_mp : unit -> ModPath.t +val make_kn : Id.t -> KerName.t (** Are we inside an opened section *) val sections_are_opened : unit -> bool @@ -97,19 +97,19 @@ val is_modtype : unit -> bool if the latest module started is a module type. *) val is_modtype_strict : unit -> bool val is_module : unit -> bool -val current_mod_id : unit -> Names.module_ident +val current_mod_id : unit -> module_ident (** Returns the opening node of a given name *) -val find_opening_node : Names.Id.t -> node +val find_opening_node : Id.t -> node (** {6 Modules and module types } *) val start_module : - export -> Names.module_ident -> Names.ModPath.t -> + export -> module_ident -> ModPath.t -> Summary.frozen -> Libnames.object_prefix val start_modtype : - Names.module_ident -> Names.ModPath.t -> + module_ident -> ModPath.t -> Summary.frozen -> Libnames.object_prefix val end_module : @@ -124,23 +124,23 @@ val end_modtype : (** {6 Compilation units } *) -val start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit -val end_compilation_checks : Names.DirPath.t -> Libnames.object_name +val start_compilation : DirPath.t -> ModPath.t -> unit +val end_compilation_checks : DirPath.t -> Libnames.object_name val end_compilation : Libnames.object_name-> Libnames.object_prefix * library_segment (** The function [library_dp] returns the [DirPath.t] of the current compiling library (or [default_library]) *) -val library_dp : unit -> Names.DirPath.t +val library_dp : unit -> DirPath.t (** Extract the library part of a name even if in a section *) -val dp_of_mp : Names.ModPath.t -> Names.DirPath.t -val split_modpath : Names.ModPath.t -> Names.DirPath.t * Names.Id.t list -val library_part : Globnames.global_reference -> Names.DirPath.t +val dp_of_mp : ModPath.t -> DirPath.t +val split_modpath : ModPath.t -> DirPath.t * Id.t list +val library_part : GlobRef.t -> DirPath.t (** {6 Sections } *) -val open_section : Names.Id.t -> unit +val open_section : Id.t -> unit val close_section : unit -> unit (** {6 We can get and set the state of the operations (used in [States]). } *) @@ -164,31 +164,31 @@ type abstr_info = private { (** Universe quantification, same length as the substitution *) } -val instance_from_variable_context : variable_context -> Names.Id.t array +val instance_from_variable_context : variable_context -> Id.t array val named_of_variable_context : variable_context -> Context.Named.t -val section_segment_of_constant : Names.Constant.t -> abstr_info -val section_segment_of_mutual_inductive: Names.MutInd.t -> abstr_info -val section_segment_of_reference : Globnames.global_reference -> abstr_info +val section_segment_of_constant : Constant.t -> abstr_info +val section_segment_of_mutual_inductive: MutInd.t -> abstr_info +val section_segment_of_reference : GlobRef.t -> abstr_info -val variable_section_segment_of_reference : Globnames.global_reference -> variable_context +val variable_section_segment_of_reference : GlobRef.t -> variable_context -val section_instance : Globnames.global_reference -> Univ.Instance.t * Names.Id.t array -val is_in_section : Globnames.global_reference -> bool +val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array +val is_in_section : GlobRef.t -> bool -val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit +val add_section_variable : Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit val add_section_context : Univ.ContextSet.t -> unit val add_section_constant : Decl_kinds.polymorphic -> - Names.Constant.t -> Context.Named.t -> unit + Constant.t -> Context.Named.t -> unit val add_section_kn : Decl_kinds.polymorphic -> - Names.MutInd.t -> Context.Named.t -> unit + MutInd.t -> Context.Named.t -> unit val replacement_context : unit -> Opaqueproof.work_list (** {6 Discharge: decrease the section level if in the current section } *) -val discharge_kn : Names.MutInd.t -> Names.MutInd.t -val discharge_con : Names.Constant.t -> Names.Constant.t -val discharge_global : Globnames.global_reference -> Globnames.global_reference -val discharge_inductive : Names.inductive -> Names.inductive +val discharge_kn : MutInd.t -> MutInd.t +val discharge_con : Constant.t -> Constant.t +val discharge_global : GlobRef.t -> GlobRef.t +val discharge_inductive : inductive -> inductive val discharge_abstract_universe_context : abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t diff --git a/library/nametab.mli b/library/nametab.mli index cd28518ab..2ec73a986 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -75,7 +75,7 @@ val error_global_not_found : qualid CAst.t -> 'a type visibility = Until of int | Exactly of int -val push : visibility -> full_path -> global_reference -> unit +val push : visibility -> full_path -> GlobRef.t -> unit val push_modtype : visibility -> full_path -> ModPath.t -> unit val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit val push_syndef : visibility -> full_path -> syndef_name -> unit @@ -91,7 +91,7 @@ val push_universe : visibility -> full_path -> universe_id -> unit (** These functions globalize a (partially) qualified name or fail with [Not_found] *) -val locate : qualid -> global_reference +val locate : qualid -> GlobRef.t val locate_extended : qualid -> extended_global_reference val locate_constant : qualid -> Constant.t val locate_syndef : qualid -> syndef_name @@ -105,20 +105,20 @@ val locate_universe : qualid -> universe_id references, like [locate] and co, but raise a nice error message in case of failure *) -val global : reference -> global_reference +val global : reference -> GlobRef.t val global_inductive : reference -> inductive (** These functions locate all global references with a given suffix; if [qualid] is valid as such, it comes first in the list *) -val locate_all : qualid -> global_reference list +val locate_all : qualid -> GlobRef.t list val locate_extended_all : qualid -> extended_global_reference list val locate_extended_all_dir : qualid -> global_dir_reference list val locate_extended_all_modtype : qualid -> ModPath.t list (** Mapping a full path to a global reference *) -val global_of_path : full_path -> global_reference +val global_of_path : full_path -> GlobRef.t val extended_global_of_path : full_path -> extended_global_reference (** {6 These functions tell if the given absolute name is already taken } *) @@ -144,7 +144,7 @@ val full_name_module : qualid -> DirPath.t definition, and the (full) dirpath associated to a module path *) val path_of_syndef : syndef_name -> full_path -val path_of_global : global_reference -> full_path +val path_of_global : GlobRef.t -> full_path val dirpath_of_module : ModPath.t -> DirPath.t val path_of_modtype : ModPath.t -> full_path @@ -155,12 +155,12 @@ val path_of_universe : universe_id -> full_path (** Returns in particular the dirpath or the basename of the full path associated to global reference *) -val dirpath_of_global : global_reference -> DirPath.t -val basename_of_global : global_reference -> Id.t +val dirpath_of_global : GlobRef.t -> DirPath.t +val basename_of_global : GlobRef.t -> Id.t (** Printing of global references using names as short as possible. @raise Not_found when the reference is not in the global tables. *) -val pr_global_env : Id.Set.t -> global_reference -> Pp.t +val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t (** The [shortest_qualid] functions given an object with [user_name] @@ -168,7 +168,7 @@ val pr_global_env : Id.Set.t -> global_reference -> Pp.t Coq.A.B.x that denotes the same object. @raise Not_found for unknown objects. *) -val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid +val shortest_qualid_of_global : Id.Set.t -> GlobRef.t -> qualid val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid val shortest_qualid_of_modtype : ModPath.t -> qualid val shortest_qualid_of_module : ModPath.t -> qualid @@ -177,7 +177,7 @@ val shortest_qualid_of_universe : universe_id -> qualid (** Deprecated synonyms *) val extended_locate : qualid -> extended_global_reference (*= locate_extended *) -val absolute_reference : full_path -> global_reference (** = global_of_path *) +val absolute_reference : full_path -> GlobRef.t (** = global_of_path *) (** {5 Generic name handling} *) diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 78545c8bd..07237d750 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Globnames open Miniml (** By default, in module Format, you can do horizontal placing of blocks @@ -54,7 +53,7 @@ val opened_libraries : unit -> ModPath.t list type kind = Term | Type | Cons | Mod -val pp_global : kind -> global_reference -> string +val pp_global : kind -> GlobRef.t -> string val pp_module : ModPath.t -> string val top_visible_mp : unit -> ModPath.t diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 397cb2920..bebd27e11 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -79,7 +79,7 @@ module type VISIT = sig (* Add reference / ... in the visit lists. These functions silently add the mp of their arg in the mp list *) - val add_ref : global_reference -> unit + val add_ref : GlobRef.t -> unit val add_kn : KerName.t -> unit val add_decl_deps : ml_decl -> unit val add_spec_deps : ml_spec -> unit diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 591d3bb86..77f1fb5ef 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -12,7 +12,6 @@ open Names open Libnames -open Globnames val simple_extraction : reference -> unit val full_extraction : string option -> reference list -> unit @@ -26,7 +25,7 @@ val extract_and_compile : reference list -> unit (* For debug / external output via coqtop.byte + Drop : *) val mono_environment : - global_reference list -> ModPath.t list -> Miniml.ml_structure + GlobRef.t list -> ModPath.t list -> Miniml.ml_structure (* Used by the Relation Extraction plugin *) diff --git a/plugins/extraction/miniml.ml b/plugins/extraction/miniml.ml index e1e49d926..ce920ad6a 100644 --- a/plugins/extraction/miniml.ml +++ b/plugins/extraction/miniml.ml @@ -11,7 +11,6 @@ (*s Target language for extraction: a core ML called MiniML. *) open Names -open Globnames (* The [signature] type is used to know how many arguments a CIC object expects, and what these arguments will become in the ML @@ -26,7 +25,7 @@ open Globnames type kill_reason = | Ktype | Kprop - | Kimplicit of global_reference * int (* n-th arg of a cst or construct *) + | Kimplicit of GlobRef.t * int (* n-th arg of a cst or construct *) type sign = Keep | Kill of kill_reason @@ -39,7 +38,7 @@ type signature = sign list type ml_type = | Tarr of ml_type * ml_type - | Tglob of global_reference * ml_type list + | Tglob of GlobRef.t * ml_type list | Tvar of int | Tvar' of int (* same as Tvar, used to avoid clash *) | Tmeta of ml_meta (* used during ML type reconstruction *) @@ -60,7 +59,7 @@ type inductive_kind = | Singleton | Coinductive | Standard - | Record of global_reference option list (* None for anonymous field *) + | Record of GlobRef.t option list (* None for anonymous field *) (* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body]. If the inductive is logical ([ip_logical = false]), then all other fields @@ -118,8 +117,8 @@ and ml_ast = | MLapp of ml_ast * ml_ast list | MLlam of ml_ident * ml_ast | MLletin of ml_ident * ml_ast * ml_ast - | MLglob of global_reference - | MLcons of ml_type * global_reference * ml_ast list + | MLglob of GlobRef.t + | MLcons of ml_type * GlobRef.t * ml_ast list | MLtuple of ml_ast list | MLcase of ml_type * ml_ast * ml_branch array | MLfix of int * Id.t array * ml_ast array @@ -129,24 +128,24 @@ and ml_ast = | MLmagic of ml_ast and ml_pattern = - | Pcons of global_reference * ml_pattern list + | Pcons of GlobRef.t * ml_pattern list | Ptuple of ml_pattern list | Prel of int (** Cf. the idents in the branch. [Prel 1] is the last one. *) | Pwild - | Pusual of global_reference (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **) + | Pusual of GlobRef.t (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **) (*s ML declarations. *) type ml_decl = | Dind of MutInd.t * ml_ind - | Dtype of global_reference * Id.t list * ml_type - | Dterm of global_reference * ml_ast * ml_type - | Dfix of global_reference array * ml_ast array * ml_type array + | Dtype of GlobRef.t * Id.t list * ml_type + | Dterm of GlobRef.t * ml_ast * ml_type + | Dfix of GlobRef.t array * ml_ast array * ml_type array type ml_spec = | Sind of MutInd.t * ml_ind - | Stype of global_reference * Id.t list * ml_type option - | Sval of global_reference * ml_type + | Stype of GlobRef.t * Id.t list * ml_type option + | Sval of GlobRef.t * ml_type type ml_specif = | Spec of ml_spec diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index e1e49d926..ce920ad6a 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -11,7 +11,6 @@ (*s Target language for extraction: a core ML called MiniML. *) open Names -open Globnames (* The [signature] type is used to know how many arguments a CIC object expects, and what these arguments will become in the ML @@ -26,7 +25,7 @@ open Globnames type kill_reason = | Ktype | Kprop - | Kimplicit of global_reference * int (* n-th arg of a cst or construct *) + | Kimplicit of GlobRef.t * int (* n-th arg of a cst or construct *) type sign = Keep | Kill of kill_reason @@ -39,7 +38,7 @@ type signature = sign list type ml_type = | Tarr of ml_type * ml_type - | Tglob of global_reference * ml_type list + | Tglob of GlobRef.t * ml_type list | Tvar of int | Tvar' of int (* same as Tvar, used to avoid clash *) | Tmeta of ml_meta (* used during ML type reconstruction *) @@ -60,7 +59,7 @@ type inductive_kind = | Singleton | Coinductive | Standard - | Record of global_reference option list (* None for anonymous field *) + | Record of GlobRef.t option list (* None for anonymous field *) (* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body]. If the inductive is logical ([ip_logical = false]), then all other fields @@ -118,8 +117,8 @@ and ml_ast = | MLapp of ml_ast * ml_ast list | MLlam of ml_ident * ml_ast | MLletin of ml_ident * ml_ast * ml_ast - | MLglob of global_reference - | MLcons of ml_type * global_reference * ml_ast list + | MLglob of GlobRef.t + | MLcons of ml_type * GlobRef.t * ml_ast list | MLtuple of ml_ast list | MLcase of ml_type * ml_ast * ml_branch array | MLfix of int * Id.t array * ml_ast array @@ -129,24 +128,24 @@ and ml_ast = | MLmagic of ml_ast and ml_pattern = - | Pcons of global_reference * ml_pattern list + | Pcons of GlobRef.t * ml_pattern list | Ptuple of ml_pattern list | Prel of int (** Cf. the idents in the branch. [Prel 1] is the last one. *) | Pwild - | Pusual of global_reference (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **) + | Pusual of GlobRef.t (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **) (*s ML declarations. *) type ml_decl = | Dind of MutInd.t * ml_ind - | Dtype of global_reference * Id.t list * ml_type - | Dterm of global_reference * ml_ast * ml_type - | Dfix of global_reference array * ml_ast array * ml_type array + | Dtype of GlobRef.t * Id.t list * ml_type + | Dterm of GlobRef.t * ml_ast * ml_type + | Dfix of GlobRef.t array * ml_ast array * ml_type array type ml_spec = | Sind of MutInd.t * ml_ind - | Stype of global_reference * Id.t list * ml_type option - | Sval of global_reference * ml_type + | Stype of GlobRef.t * Id.t list * ml_type option + | Sval of GlobRef.t * ml_type type ml_specif = | Spec of ml_spec diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 0656d487a..0901acc7d 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -59,7 +59,7 @@ let rec eq_ml_type t1 t2 = match t1, t2 with | Tarr (tl1, tr1), Tarr (tl2, tr2) -> eq_ml_type tl1 tl2 && eq_ml_type tr1 tr2 | Tglob (gr1, t1), Tglob (gr2, t2) -> - eq_gr gr1 gr2 && List.equal eq_ml_type t1 t2 + GlobRef.equal gr1 gr2 && List.equal eq_ml_type t1 t2 | Tvar i1, Tvar i2 -> Int.equal i1 i2 | Tvar' i1, Tvar' i2 -> Int.equal i1 i2 | Tmeta m1, Tmeta m2 -> eq_ml_meta m1 m2 @@ -120,7 +120,7 @@ let rec mgu = function | None -> m.contents <- Some t) | Tarr(a, b), Tarr(a', b') -> mgu (a, a'); mgu (b, b') - | Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' -> + | Tglob (r,l), Tglob (r',l') when GlobRef.equal r r' -> List.iter mgu (List.combine l l') | Tdummy _, Tdummy _ -> () | Tvar i, Tvar j when Int.equal i j -> () @@ -270,7 +270,7 @@ let rec var2var' = function | Tglob (r,l) -> Tglob (r, List.map var2var' l) | a -> a -type abbrev_map = global_reference -> ml_type option +type abbrev_map = GlobRef.t -> ml_type option (*s Delta-reduction of type constants everywhere in a ML type [t]. [env] is a function of type [ml_type_env]. *) @@ -381,9 +381,9 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with eq_ml_ident na1 na2 && eq_ml_ast t1 t2 | MLletin (na1, c1, t1), MLletin (na2, c2, t2) -> eq_ml_ident na1 na2 && eq_ml_ast c1 c2 && eq_ml_ast t1 t2 -| MLglob gr1, MLglob gr2 -> eq_gr gr1 gr2 +| MLglob gr1, MLglob gr2 -> GlobRef.equal gr1 gr2 | MLcons (t1, gr1, c1), MLcons (t2, gr2, c2) -> - eq_ml_type t1 t2 && eq_gr gr1 gr2 && List.equal eq_ml_ast c1 c2 + eq_ml_type t1 t2 && GlobRef.equal gr1 gr2 && List.equal eq_ml_ast c1 c2 | MLtuple t1, MLtuple t2 -> List.equal eq_ml_ast t1 t2 | MLcase (t1, c1, p1), MLcase (t2, c2, p2) -> @@ -398,13 +398,13 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with and eq_ml_pattern p1 p2 = match p1, p2 with | Pcons (gr1, p1), Pcons (gr2, p2) -> - eq_gr gr1 gr2 && List.equal eq_ml_pattern p1 p2 + GlobRef.equal gr1 gr2 && List.equal eq_ml_pattern p1 p2 | Ptuple p1, Ptuple p2 -> List.equal eq_ml_pattern p1 p2 | Prel i1, Prel i2 -> Int.equal i1 i2 | Pwild, Pwild -> true -| Pusual gr1, Pusual gr2 -> eq_gr gr1 gr2 +| Pusual gr1, Pusual gr2 -> GlobRef.equal gr1 gr2 | _ -> false and eq_ml_branch (id1, p1, t1) (id2, p2, t2) = @@ -984,7 +984,7 @@ let rec iota_red i lift br ((typ,r,a) as cons) = if i >= Array.length br then raise Impossible; let (ids,p,c) = br.(i) in match p with - | Pusual r' | Pcons (r',_) when not (Globnames.eq_gr r' r) -> iota_red (i+1) lift br cons + | Pusual r' | Pcons (r',_) when not (GlobRef.equal r' r) -> iota_red (i+1) lift br cons | Pusual r' -> let c = named_lams (List.rev ids) c in let c = ast_lift lift c diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 55a1ee893..d23fdb3d5 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Globnames open Miniml open Table @@ -59,7 +58,7 @@ val type_recomp : ml_type list * ml_type -> ml_type val var2var' : ml_type -> ml_type -type abbrev_map = global_reference -> ml_type option +type abbrev_map = GlobRef.t -> ml_type option val type_expand : abbrev_map -> ml_type -> ml_type val type_simpl : ml_type -> ml_type @@ -117,7 +116,7 @@ val dump_unused_vars : ml_ast -> ml_ast val normalize : ml_ast -> ml_ast val optimize_fix : ml_ast -> ml_ast -val inline : global_reference -> ml_ast -> bool +val inline : GlobRef.t -> ml_ast -> bool val is_basic_pattern : ml_pattern -> bool val has_deep_pattern : ml_branch array -> bool diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index f33a59edf..b398bc07a 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -76,7 +76,7 @@ let struct_iter do_decl do_spec do_mp s = (*s Apply some fonctions upon all references in [ml_type], [ml_ast], [ml_decl], [ml_spec] and [ml_structure]. *) -type do_ref = global_reference -> unit +type do_ref = GlobRef.t -> unit let record_iter_references do_term = function | Record l -> List.iter (Option.iter do_term) l diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli index 6a81f2705..f45773f09 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Globnames open Miniml (*s Functions upon ML modules. *) @@ -17,7 +16,7 @@ open Miniml val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool val struct_type_search : (ml_type -> bool) -> ml_structure -> bool -type do_ref = global_reference -> unit +type do_ref = GlobRef.t -> unit val type_iter_references : do_ref -> ml_type -> unit val ast_iter_references : do_ref -> do_ref -> do_ref -> ml_ast -> unit @@ -30,7 +29,7 @@ val mtyp_of_mexpr : ml_module_expr -> ml_module_type val msid_of_mt : ml_module_type -> ModPath.t -val get_decl_in_structure : global_reference -> ml_structure -> ml_decl +val get_decl_in_structure : GlobRef.t -> ml_structure -> ml_decl (* Some transformations of ML terms. [optimize_struct] simplify all beta redexes (when the argument does not occur, it is just @@ -39,5 +38,5 @@ val get_decl_in_structure : global_reference -> ml_structure -> ml_decl optimizations. The first argument is the list of objects we want to appear. *) -val optimize_struct : global_reference list * ModPath.t list -> +val optimize_struct : GlobRef.t list * ModPath.t list -> ml_structure -> ml_structure diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 54c6d9d72..c3f4cfe65 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -652,7 +652,7 @@ let add_inline_entries b l = (* Registration of operations for rollback. *) -let inline_extraction : bool * global_reference list -> obj = +let inline_extraction : bool * GlobRef.t list -> obj = declare_object {(default_object "Extraction Inline") with cache_function = (fun (_,(b,l)) -> add_inline_entries b l); @@ -736,7 +736,7 @@ let add_implicits r l = (* Registration of operations for rollback. *) -let implicit_extraction : global_reference * int_or_id list -> obj = +let implicit_extraction : GlobRef.t * int_or_id list -> obj = declare_object {(default_object "Extraction Implicit") with cache_function = (fun (_,(r,l)) -> add_implicits r l); @@ -857,7 +857,7 @@ let find_custom_match pv = (* Registration of operations for rollback. *) -let in_customs : global_reference * string list * string -> obj = +let in_customs : GlobRef.t * string list * string -> obj = declare_object {(default_object "ML extractions") with cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s); @@ -867,7 +867,7 @@ let in_customs : global_reference * string list * string -> obj = (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str)) } -let in_custom_matchs : global_reference * string -> obj = +let in_custom_matchs : GlobRef.t * string -> obj = declare_object {(default_object "ML extractions custom matchs") with cache_function = (fun (_,(r,s)) -> add_custom_match r s); diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 906dfd96e..5bf944434 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -10,31 +10,30 @@ open Names open Libnames -open Globnames open Miniml open Declarations -module Refset' : CSig.SetS with type elt = global_reference -module Refmap' : CSig.MapS with type key = global_reference +module Refset' : CSig.SetS with type elt = GlobRef.t +module Refmap' : CSig.MapS with type key = GlobRef.t -val safe_basename_of_global : global_reference -> Id.t +val safe_basename_of_global : GlobRef.t -> Id.t (*s Warning and Error messages. *) val warning_axioms : unit -> unit val warning_opaques : bool -> unit -val warning_ambiguous_name : ?loc:Loc.t -> qualid * ModPath.t * global_reference -> unit +val warning_ambiguous_name : ?loc:Loc.t -> qualid * ModPath.t * GlobRef.t -> unit val warning_id : string -> unit -val error_axiom_scheme : global_reference -> int -> 'a -val error_constant : global_reference -> 'a -val error_inductive : global_reference -> 'a +val error_axiom_scheme : GlobRef.t -> int -> 'a +val error_constant : GlobRef.t -> 'a +val error_inductive : GlobRef.t -> 'a val error_nb_cons : unit -> 'a val error_module_clash : ModPath.t -> ModPath.t -> 'a val error_no_module_expr : ModPath.t -> 'a -val error_singleton_become_prop : Id.t -> global_reference option -> 'a +val error_singleton_become_prop : Id.t -> GlobRef.t option -> 'a val error_unknown_module : qualid -> 'a val error_scheme : unit -> 'a -val error_not_visible : global_reference -> 'a +val error_not_visible : GlobRef.t -> 'a val error_MPfile_as_mod : ModPath.t -> bool -> 'a val check_inside_module : unit -> unit val check_inside_section : unit -> unit @@ -44,12 +43,12 @@ val err_or_warn_remaining_implicit : kill_reason -> unit val info_file : string -> unit -(*s utilities about [module_path] and [kernel_names] and [global_reference] *) +(*s utilities about [module_path] and [kernel_names] and [GlobRef.t] *) -val occur_kn_in_ref : MutInd.t -> global_reference -> bool -val repr_of_r : global_reference -> ModPath.t * DirPath.t * Label.t -val modpath_of_r : global_reference -> ModPath.t -val label_of_r : global_reference -> Label.t +val occur_kn_in_ref : MutInd.t -> GlobRef.t -> bool +val repr_of_r : GlobRef.t -> ModPath.t * DirPath.t * Label.t +val modpath_of_r : GlobRef.t -> ModPath.t +val label_of_r : GlobRef.t -> Label.t val base_mp : ModPath.t -> ModPath.t val is_modfile : ModPath.t -> bool val string_of_modfile : ModPath.t -> string @@ -61,7 +60,7 @@ val prefixes_mp : ModPath.t -> MPset.t val common_prefix_from_list : ModPath.t -> ModPath.t list -> ModPath.t option val get_nth_label_mp : int -> ModPath.t -> Label.t -val labels_of_ref : global_reference -> ModPath.t * Label.t list +val labels_of_ref : GlobRef.t -> ModPath.t * Label.t list (*s Some table-related operations *) @@ -83,27 +82,27 @@ val add_ind : MutInd.t -> mutual_inductive_body -> ml_ind -> unit val lookup_ind : MutInd.t -> mutual_inductive_body -> ml_ind option val add_inductive_kind : MutInd.t -> inductive_kind -> unit -val is_coinductive : global_reference -> bool +val is_coinductive : GlobRef.t -> bool val is_coinductive_type : ml_type -> bool (* What are the fields of a record (empty for a non-record) *) val get_record_fields : - global_reference -> global_reference option list -val record_fields_of_type : ml_type -> global_reference option list + GlobRef.t -> GlobRef.t option list +val record_fields_of_type : ml_type -> GlobRef.t option list val add_recursors : Environ.env -> MutInd.t -> unit -val is_recursor : global_reference -> bool +val is_recursor : GlobRef.t -> bool val add_projection : int -> Constant.t -> inductive -> unit -val is_projection : global_reference -> bool -val projection_arity : global_reference -> int -val projection_info : global_reference -> inductive * int (* arity *) +val is_projection : GlobRef.t -> bool +val projection_arity : GlobRef.t -> int +val projection_info : GlobRef.t -> inductive * int (* arity *) -val add_info_axiom : global_reference -> unit -val remove_info_axiom : global_reference -> unit -val add_log_axiom : global_reference -> unit +val add_info_axiom : GlobRef.t -> unit +val remove_info_axiom : GlobRef.t -> unit +val add_log_axiom : GlobRef.t -> unit -val add_opaque : global_reference -> unit -val remove_opaque : global_reference -> unit +val add_opaque : GlobRef.t -> unit +val remove_opaque : GlobRef.t -> unit val reset_tables : unit -> unit @@ -172,22 +171,22 @@ val is_extrcompute : unit -> bool (*s Table for custom inlining *) -val to_inline : global_reference -> bool -val to_keep : global_reference -> bool +val to_inline : GlobRef.t -> bool +val to_keep : GlobRef.t -> bool (*s Table for implicits arguments *) -val implicits_of_global : global_reference -> Int.Set.t +val implicits_of_global : GlobRef.t -> Int.Set.t (*s Table for user-given custom ML extractions. *) (* UGLY HACK: registration of a function defined in [extraction.ml] *) val type_scheme_nb_args_hook : (Environ.env -> Constr.t -> int) Hook.t -val is_custom : global_reference -> bool -val is_inline_custom : global_reference -> bool -val find_custom : global_reference -> string -val find_type_custom : global_reference -> string list * string +val is_custom : GlobRef.t -> bool +val is_inline_custom : GlobRef.t -> bool +val find_custom : GlobRef.t -> string +val find_type_custom : GlobRef.t -> string list * string val is_custom_match : ml_branch array -> bool val find_custom_match : ml_branch array -> string diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 047fc9fbf..a60a966ce 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -211,7 +211,7 @@ type left_pattern= | Lexists of pinductive | LA of constr*left_arrow_pattern -type t={id:global_reference; +type t={id:GlobRef.t; constr:constr; pat:(left_pattern,right_pattern) sum; atoms:atoms} diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 2962d9230..e2c6f1c4b 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -8,9 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open Constr open EConstr -open Globnames val qflag : bool ref @@ -35,7 +35,7 @@ type atoms = {positive:constr list;negative:constr list} type side = Hyp | Concl | Hint -val dummy_id: global_reference +val dummy_id: GlobRef.t val build_atoms : Environ.env -> Evd.evar_map -> counter -> side -> constr -> bool * atoms @@ -65,13 +65,13 @@ type left_pattern= | Lexists of pinductive | LA of constr*left_arrow_pattern -type t={id: global_reference; +type t={id: GlobRef.t; constr: constr; pat: (left_pattern,right_pattern) sum; atoms: atoms} (*exception Is_atom of constr*) -val build_formula : Environ.env -> Evd.evar_map -> side -> global_reference -> types -> +val build_formula : Environ.env -> Evd.evar_map -> side -> GlobRef.t -> types -> counter -> (t,types) sum diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index e8c0b927d..22a3e1f67 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -43,7 +43,7 @@ let compare_gr id1 id2 = module OrderedInstance= struct - type t=instance * Globnames.global_reference + type t=instance * GlobRef.t let compare (inst1,id1) (inst2,id2)= (compare_instance =? compare_gr) inst2 inst1 id2 id1 (* we want a __decreasing__ total order *) diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli index 61786ffdc..9f9ade3aa 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -8,13 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Globnames +open Names open Rules val collect_quantified : Evd.evar_map -> Sequent.t -> Formula.t list * Sequent.t val give_instances : Evd.evar_map -> Formula.t list -> Sequent.t -> - (Unify.instance * global_reference) list + (Unify.instance * GlobRef.t) list val quantified_tac : Formula.t list -> seqtac with_backtracking diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index cfcd65619..2d7a3e37b 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -29,7 +29,7 @@ type tactic = unit Proofview.tactic type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic -type lseqtac= global_reference -> seqtac +type lseqtac= GlobRef.t -> seqtac type 'a with_backtracking = tactic -> 'a diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index 859388b30..924c26790 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -11,21 +11,20 @@ open Names open Constr open EConstr -open Globnames type tactic = unit Proofview.tactic type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic -type lseqtac= global_reference -> seqtac +type lseqtac= GlobRef.t -> seqtac type 'a with_backtracking = tactic -> 'a val wrap : int -> bool -> seqtac -val basename_of_global: global_reference -> Id.t +val basename_of_global: GlobRef.t -> Id.t -val clear_global: global_reference -> tactic +val clear_global: GlobRef.t -> tactic val axiom_tac : constr -> Sequent.t -> tactic @@ -41,7 +40,7 @@ val left_and_tac : pinductive -> lseqtac with_backtracking val left_or_tac : pinductive -> lseqtac with_backtracking -val left_false_tac : global_reference -> tactic +val left_false_tac : GlobRef.t -> tactic val ll_ind_tac : pinductive -> constr list -> lseqtac with_backtracking diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 7c612c0d8..0c752d4a4 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -8,13 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open EConstr -open CErrors open Util +open Pp +open CErrors +open Names +open EConstr open Formula open Unify -open Globnames -open Pp let newcnt ()= let cnt=ref (-1) in @@ -56,7 +56,7 @@ struct (priority e1.pat) - (priority e2.pat) end -type h_item = global_reference * (int*Constr.t) option +type h_item = GlobRef.t * (int*Constr.t) option module Hitem= struct @@ -87,7 +87,7 @@ let cm_remove sigma typ nam cm= let typ = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in try let l=CM.find typ cm in - let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in + let l0=List.filter (fun id-> not (GlobRef.equal id nam)) l in match l0 with []->CM.remove typ cm | _ ->CM.add typ l0 cm @@ -97,7 +97,7 @@ module HP=Heap.Functional(OrderedFormula) type t= {redexes:HP.t; - context:(global_reference list) CM.t; + context:(GlobRef.t list) CM.t; latoms:constr list; gl:types; glatom:constr option; @@ -117,7 +117,7 @@ let lookup sigma item seq= let p (id2,o)= match o with None -> false - | Some (m2, t2)-> Globnames.eq_gr id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in + | Some (m2, t2)-> GlobRef.equal id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in History.exists p seq.history let add_formula env sigma side nam t seq = @@ -187,9 +187,9 @@ let empty_seq depth= let expand_constructor_hints = List.map_append (function - | IndRef ind -> + | GlobRef.IndRef ind -> List.init (Inductiveops.nconstructors ind) - (fun i -> ConstructRef (ind,i+1)) + (fun i -> GlobRef.ConstructRef (ind,i+1)) | gr -> [gr]) diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index c4ed3e21f..709b278ec 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -8,26 +8,26 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open EConstr open Formula -open Globnames module CM: CSig.MapS with type key=Constr.t -type h_item = global_reference * (int*Constr.t) option +type h_item = GlobRef.t * (int*Constr.t) option module History: Set.S with type elt = h_item -val cm_add : Evd.evar_map -> constr -> global_reference -> global_reference list CM.t -> - global_reference list CM.t +val cm_add : Evd.evar_map -> constr -> GlobRef.t -> GlobRef.t list CM.t -> + GlobRef.t list CM.t -val cm_remove : Evd.evar_map -> constr -> global_reference -> global_reference list CM.t -> - global_reference list CM.t +val cm_remove : Evd.evar_map -> constr -> GlobRef.t -> GlobRef.t list CM.t -> + GlobRef.t list CM.t module HP: Heap.S with type elt=Formula.t type t = {redexes:HP.t; - context: global_reference list CM.t; + context: GlobRef.t list CM.t; latoms:constr list; gl:types; glatom:constr option; @@ -41,20 +41,20 @@ val record: h_item -> t -> t val lookup: Evd.evar_map -> h_item -> t -> bool -val add_formula : Environ.env -> Evd.evar_map -> side -> global_reference -> constr -> t -> t +val add_formula : Environ.env -> Evd.evar_map -> side -> GlobRef.t -> constr -> t -> t val re_add_formula_list : Evd.evar_map -> Formula.t list -> t -> t -val find_left : Evd.evar_map -> constr -> t -> global_reference +val find_left : Evd.evar_map -> constr -> t -> GlobRef.t val take_formula : Evd.evar_map -> t -> Formula.t * t val empty_seq : int -> t -val extend_with_ref_list : Environ.env -> Evd.evar_map -> global_reference list -> +val extend_with_ref_list : Environ.env -> Evd.evar_map -> GlobRef.t list -> t -> t * Evd.evar_map val extend_with_auto_hints : Environ.env -> Evd.evar_map -> Hints.hint_db_name list -> t -> t * Evd.evar_map -val print_cmap: global_reference list CM.t -> Pp.t +val print_cmap: GlobRef.t list CM.t -> Pp.t diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index b1c003de2..0ea70c19f 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -227,7 +227,7 @@ let ineq1_of_constr (h,t) = hstrict=false}] |_-> raise NoIneq) | Ind ((kn,i),_) -> - if not (eq_gr (IndRef(kn,i)) Coqlib.glob_eq) then raise NoIneq; + if not (GlobRef.equal (IndRef(kn,i)) Coqlib.glob_eq) then raise NoIneq; let t0= args.(0) in let t1= args.(1) in let t2= args.(2) in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 319b410df..3ba3bafa4 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -885,7 +885,7 @@ let is_res r = match DAst.get r with | _ -> false let is_gr c gr = match DAst.get c with -| GRef (r, _) -> Globnames.eq_gr r gr +| GRef (r, _) -> GlobRef.equal r gr | _ -> false let is_gvar c = match DAst.get c with @@ -894,7 +894,7 @@ let is_gvar c = match DAst.get c with let same_raw_term rt1 rt2 = match DAst.get rt1, DAst.get rt2 with - | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2 + | GRef(r1,_), GRef (r2,_) -> GlobRef.equal r1 r2 | GHole _, GHole _ -> true | _ -> false let decompose_raw_eq lhs rhs = diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index e331dc014..ae238b846 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -576,7 +576,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas (fun _ evi _ -> match evi.evar_source with | (loc_evi,ImplicitArg(gr_evi,p_evi,b_evi)) -> - if Globnames.eq_gr grk gr_evi && pk=p_evi && bk=b_evi && rt.CAst.loc = loc_evi + if GlobRef.equal grk gr_evi && pk=p_evi && bk=b_evi && rt.CAst.loc = loc_evi then raise (Found evi) | _ -> () ) diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 7088ae596..481a8be3b 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -13,7 +13,7 @@ val pattern_to_term : cases_pattern -> glob_constr Some basic functions to rebuild glob_constr In each of them the location is Util.Loc.ghost *) -val mkGRef : Globnames.global_reference -> glob_constr +val mkGRef : GlobRef.t -> glob_constr val mkGVar : Id.t -> glob_constr val mkGApp : glob_constr*(glob_constr list) -> glob_constr val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 748d8add2..7df57b577 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -846,7 +846,7 @@ let rec get_args b t : Constrexpr.local_binder_expr list * | _ -> [],b,t -let make_graph (f_ref:global_reference) = +let make_graph (f_ref : GlobRef.t) = let c,c_body = match f_ref with | ConstRef c -> diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index dcc1c2ea6..24304e361 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,3 +1,4 @@ +open Names open Misctypes val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit @@ -18,4 +19,4 @@ val functional_induction : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma -val make_graph : Globnames.global_reference -> unit +val make_graph : GlobRef.t -> unit diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 5cc7163aa..346b21ef2 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -41,7 +41,7 @@ val chop_rprod_n : int -> Glob_term.glob_constr -> val def_of_const : Constr.t -> Constr.t val eq : EConstr.constr Lazy.t val refl_equal : EConstr.constr Lazy.t -val const_of_id: Id.t -> Globnames.global_reference(* constantyes *) +val const_of_id: Id.t -> GlobRef.t(* constantyes *) val jmeq : unit -> EConstr.constr val jmeq_refl : unit -> EConstr.constr @@ -107,11 +107,11 @@ val h_intros: Names.Id.t list -> Tacmach.tactic val h_id : Names.Id.t val hrec_id : Names.Id.t val acc_inv_id : EConstr.constr Util.delayed -val ltof_ref : Globnames.global_reference Util.delayed +val ltof_ref : GlobRef.t Util.delayed val well_founded_ltof : EConstr.constr Util.delayed val acc_rel : EConstr.constr Util.delayed val well_founded : EConstr.constr Util.delayed -val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference +val evaluable_of_global_reference : GlobRef.t -> Names.evaluable_global_reference val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic val decompose_lam_n : Evd.evar_map -> int -> EConstr.t -> diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli index ad306ab25..9151fd0e2 100644 --- a/plugins/funind/invfun.mli +++ b/plugins/funind/invfun.mli @@ -10,7 +10,7 @@ val invfun : Misctypes.quantified_hypothesis -> - Globnames.global_reference option -> + Names.GlobRef.t option -> Evar.t Evd.sigma -> Evar.t list Evd.sigma val derive_correctness : (Evd.evar_map ref -> diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index e41bf71dd..2a3a85fcc 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -181,7 +181,7 @@ let simpl_iter clause = clause (* Others ugly things ... *) -let (value_f: Constr.t list -> global_reference -> Constr.t) = +let (value_f: Constr.t list -> GlobRef.t -> Constr.t) = let open Term in let open Constr in fun al fterm -> @@ -215,7 +215,7 @@ let (value_f: Constr.t list -> global_reference -> Constr.t) = let body = EConstr.Unsafe.to_constr body in it_mkLambda_or_LetIn body context -let (declare_f : Id.t -> logical_kind -> Constr.t list -> global_reference -> global_reference) = +let (declare_f : Id.t -> logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) = fun f_id kind input_type fterm_ref -> declare_fun f_id kind (value_f input_type fterm_ref);; @@ -356,7 +356,7 @@ type 'a infos = f_id : Id.t; (* function name *) f_constr : constr; (* function term *) f_terminate : constr; (* termination proof term *) - func : global_reference; (* functional reference *) + func : GlobRef.t; (* functional reference *) info : 'a; is_main_branch : bool; (* on the main branch or on a matched expression *) is_final : bool; (* final first order term or not *) @@ -1456,7 +1456,7 @@ let com_terminate -let start_equation (f:global_reference) (term_f:global_reference) +let start_equation (f:GlobRef.t) (term_f:GlobRef.t) (cont_tactic:Id.t list -> tactic) g = let sigma = project g in let ids = pf_ids_of_hyps g in @@ -1473,7 +1473,7 @@ let start_equation (f:global_reference) (term_f:global_reference) observe_tac (str "prove_eq") (cont_tactic x)]) g;; let (com_eqn : int -> Id.t -> - global_reference -> global_reference -> global_reference + GlobRef.t -> GlobRef.t -> GlobRef.t -> Constr.t -> unit) = fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type -> let open CVars in diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 1fa5e3c07..5185217cd 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -80,7 +80,7 @@ val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Id.t val coerce_to_hyp_list : Environ.env -> Evd.evar_map -> Value.t -> Id.t list -val coerce_to_reference : Environ.env -> Evd.evar_map -> Value.t -> Globnames.global_reference +val coerce_to_reference : Environ.env -> Evd.evar_map -> Value.t -> GlobRef.t val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypothesis diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 33c30e4d3..5facf2a80 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -78,7 +78,7 @@ and mk_clos_app_but f_map subs f args n = | None -> mk_atom (mkApp (f, args)) let interp_map l t = - try Some(List.assoc_f eq_gr t l) with Not_found -> None + try Some(List.assoc_f GlobRef.equal t l) with Not_found -> None let protect_maps = ref String.Map.empty let add_map s m = protect_maps := String.Map.add s m !protect_maps diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index 1d1557b12..0e056a472 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -11,7 +11,6 @@ open Names open EConstr open Libnames -open Globnames open Constrexpr open Newring_ast @@ -19,7 +18,7 @@ val protect_tac_in : string -> Id.t -> unit Proofview.tactic val protect_tac : string -> unit Proofview.tactic -val closed_term : EConstr.constr -> global_reference list -> unit Proofview.tactic +val closed_term : EConstr.constr -> GlobRef.t list -> unit Proofview.tactic val add_theory : Id.t -> diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d012fd0df..e9e045a53 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1505,7 +1505,7 @@ let tclOPTION o d = let tacIS_INJECTION_CASE ?ty t = begin tclOPTION ty (tacTYPEOF t) >>= fun ty -> tacREDUCE_TO_QUANTIFIED_IND ty >>= fun ((mind,_),_) -> - tclUNIT (Globnames.eq_gr (Globnames.IndRef mind) (Coqlib.build_coq_eq ())) + tclUNIT (GlobRef.equal (GlobRef.IndRef mind) (Coqlib.build_coq_eq ())) end let tclWITHTOP tac = Goal.enter begin fun gl -> diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 2b8f1d540..9ba23467e 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -212,7 +212,7 @@ val pf_abs_prod : EConstr.t -> Goal.goal Evd.sigma * EConstr.types val mkSsrRRef : string -> Glob_term.glob_constr * 'a option -val mkSsrRef : string -> Globnames.global_reference +val mkSsrRef : string -> GlobRef.t val mkSsrConst : string -> env -> evar_map -> evar_map * EConstr.t @@ -224,7 +224,7 @@ val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx val pf_fresh_global : - Globnames.global_reference -> + GlobRef.t -> Goal.goal Evd.sigma -> Constr.constr * Goal.goal Evd.sigma diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index de8ffb976..87d107d65 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -418,7 +418,7 @@ let injectl2rtac sigma c = match EConstr.kind sigma c with let is_injection_case c gl = let gl, cty = pfe_type_of gl c in let (mind,_), _ = pf_reduce_to_quantified_ind gl cty in - eq_gr (IndRef mind) (Coqlib.build_coq_eq ()) + GlobRef.equal (IndRef mind) (Coqlib.build_coq_eq ()) let perform_injection c gl = let gl, cty = pfe_type_of gl c in diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 7748ba2b0..7d7655d29 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -369,8 +369,8 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = ;; let is_construct_ref sigma c r = - EConstr.isConstruct sigma c && eq_gr (ConstructRef (fst(EConstr.destConstruct sigma c))) r -let is_ind_ref sigma c r = EConstr.isInd sigma c && eq_gr (IndRef (fst(EConstr.destInd sigma c))) r + EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r +let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r let rwcltac cl rdx dir sr gl = let n, r_n,_, ucst = pf_abs_evars gl sr in diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index acb297ddf..47a59ba63 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -28,7 +28,7 @@ let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) let is_gr c gr = match DAst.get c with -| GRef (r, _) -> Globnames.eq_gr r gr +| GRef (r, _) -> GlobRef.equal r gr | _ -> false let ascii_module = ["Coq";"Strings";"Ascii"] diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml index 5529ea700..f10f98e23 100644 --- a/plugins/syntax/int31_syntax.ml +++ b/plugins/syntax/int31_syntax.ml @@ -26,7 +26,7 @@ let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) let is_gr c gr = match DAst.get c with -| GRef (r, _) -> Globnames.eq_gr r gr +| GRef (r, _) -> GlobRef.equal r gr | _ -> false let make_mind mp id = Names.MutInd.make2 mp (Label.make id) diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index ad8b54d4d..e158e0b51 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -16,11 +16,12 @@ let () = Mltop.add_known_module __coq_plugin_name (* This file defines the printer for natural numbers in [nat] *) (*i*) +open Pp +open CErrors +open Names open Glob_term open Bigint open Coqlib -open Pp -open CErrors (*i*) (**********************************************************************) @@ -61,10 +62,10 @@ exception Non_closed_number let rec int_of_nat x = DAst.with_val (function | GApp (r, [a]) -> begin match DAst.get r with - | GRef (s,_) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) + | GRef (s,_) when GlobRef.equal s glob_S -> add_1 (int_of_nat a) | _ -> raise Non_closed_number end - | GRef (z,_) when Globnames.eq_gr z glob_O -> zero + | GRef (z,_) when GlobRef.equal z glob_O -> zero | _ -> raise Non_closed_number ) x diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 372e8ff30..94aa14335 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -30,7 +30,7 @@ let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) let is_gr c gr = match DAst.get c with -| GRef (r, _) -> Globnames.eq_gr r gr +| GRef (r, _) -> GlobRef.equal r gr | _ -> false let positive_path = make_path binnums "positive" @@ -66,7 +66,7 @@ let pos_of_bignat ?loc x = let rec bignat_of_pos c = match DAst.get c with | GApp (r, [a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) | GApp (r, [a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a)) - | GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one + | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one | _ -> raise Non_closed_number (**********************************************************************) @@ -98,7 +98,7 @@ let z_of_int ?loc n = let bigint_of_z c = match DAst.get c with | GApp (r,[a]) when is_gr r glob_POS -> bignat_of_pos a | GApp (r,[a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a) - | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero + | GRef (a, _) when GlobRef.equal a glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number (**********************************************************************) diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index 2421cc12f..c22869f4d 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open Globnames open Ascii_syntax_plugin.Ascii_syntax open Glob_term @@ -34,7 +35,7 @@ let glob_String = lazy (make_reference "String") let glob_EmptyString = lazy (make_reference "EmptyString") let is_gr c gr = match DAst.get c with -| GRef (r, _) -> Globnames.eq_gr r gr +| GRef (r, _) -> GlobRef.equal r gr | _ -> false open Lazy @@ -55,7 +56,7 @@ let uninterp_string (AnyGlobConstr r) = (match uninterp_ascii a with | Some c -> Buffer.add_char b (Char.chr c); aux s | _ -> raise Non_closed_string) - | GRef (z,_) when eq_gr z (force glob_EmptyString) -> + | GRef (z,_) when GlobRef.equal z (force glob_EmptyString) -> Some (Buffer.contents b) | _ -> raise Non_closed_string diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index d5300e474..09fe8bf70 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -71,13 +71,13 @@ let interp_positive ?loc n = (**********************************************************************) let is_gr c gr = match DAst.get c with -| GRef (r, _) -> Globnames.eq_gr r gr +| GRef (r, _) -> GlobRef.equal r gr | _ -> false let rec bignat_of_pos x = DAst.with_val (function | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a)) - | GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one + | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one | _ -> raise Non_closed_number ) x @@ -132,7 +132,7 @@ let n_of_int ?loc n = let bignat_of_n n = DAst.with_val (function | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a - | GRef (a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero + | GRef (a,_) when GlobRef.equal a glob_N0 -> Bigint.zero | _ -> raise Non_closed_number ) n @@ -180,7 +180,7 @@ let z_of_int ?loc n = let bigint_of_z z = DAst.with_val (function | GApp (r, [a]) when is_gr r glob_POS -> bignat_of_pos a | GApp (r, [a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a) - | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero + | GRef (a, _) when GlobRef.equal a glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number ) z diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 84295959f..9d4badc60 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -26,7 +26,7 @@ let name_table = type req = | ReqLocal - | ReqGlobal of global_reference * Name.t list + | ReqGlobal of GlobRef.t * Name.t list let load_rename_args _ (_, (_, (r, names))) = name_table := Refmap.add r names !name_table diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index 65e3c3be5..6a776dc96 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -9,14 +9,13 @@ (************************************************************************) open Names -open Globnames open Environ open Constr -val rename_arguments : bool -> global_reference -> Name.t list -> unit +val rename_arguments : bool -> GlobRef.t -> Name.t list -> unit (** [Not_found] is raised if no names are defined for [r] *) -val arguments_names : global_reference -> Name.t list +val arguments_names : GlobRef.t -> Name.t list val rename_type_of_constant : env -> pconstant -> types val rename_type_of_inductive : env -> pinductive -> types diff --git a/pretyping/classops.ml b/pretyping/classops.ml index a0804b72b..afa8a12fc 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -37,7 +37,7 @@ type cl_info_typ = { cl_param : int } -type coe_typ = global_reference +type coe_typ = GlobRef.t module CoeTypMap = Refmap_env diff --git a/pretyping/classops.mli b/pretyping/classops.mli index f8600bbe0..35691ea37 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -36,7 +36,7 @@ type cl_info_typ = { cl_param : int } (** This is the type of coercion kinds *) -type coe_typ = Globnames.global_reference +type coe_typ = GlobRef.t (** This is the type of infos for declared coercions *) type coe_info_typ diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index e89bbf7c3..3ae04cd4f 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -113,7 +113,7 @@ let instance_eq f (x1,c1) (x2,c2) = Id.equal x1 x2 && f c1 c2 let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with - | GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2 + | GRef (gr1, _), GRef (gr2, _) -> GlobRef.equal gr1 gr2 | GVar id1, GVar id2 -> Id.equal id1 id2 | GEvar (id1, arg1), GEvar (id2, arg2) -> Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2 diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 84be15552..3c3f75a68 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -17,7 +17,6 @@ arguments and pattern-matching compilation are not. *) open Names -open Globnames open Decl_kinds open Misctypes @@ -36,7 +35,7 @@ type cases_pattern = [ `any ] cases_pattern_g (** Representation of an internalized (or in other words globalized) term. *) type 'a glob_constr_r = - | GRef of global_reference * glob_level list option + | GRef of GlobRef.t * glob_level list option (** An identifier that represents a reference to an object defined either in the (global) environment or in the (local) context. *) | GVar of Id.t diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 119ff5222..d87a19d28 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -61,7 +61,7 @@ val weaken_sort_scheme : env -> evar_map -> bool -> Sorts.t -> int -> constr -> (** Recursor names utilities *) -val lookup_eliminator : inductive -> Sorts.family -> Globnames.global_reference +val lookup_eliminator : inductive -> Sorts.family -> GlobRef.t val elimination_suffix : Sorts.family -> string val make_elimination_ident : Id.t -> Sorts.family -> Id.t diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 76367b612..7dd0954bc 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Globnames open Misctypes (** {5 Patterns} *) @@ -21,7 +20,7 @@ type case_info_pattern = cip_extensible : bool (** does this match end with _ => _ ? *) } type constr_pattern = - | PRef of global_reference + | PRef of GlobRef.t | PVar of Id.t | PEvar of existential_key * constr_pattern array | PRel of int diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 27e457e3b..ccfb7f990 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -30,7 +30,7 @@ let case_info_pattern_eq i1 i2 = i1.cip_extensible == i2.cip_extensible let rec constr_pattern_eq p1 p2 = match p1, p2 with -| PRef r1, PRef r2 -> eq_gr r1 r2 +| PRef r1, PRef r2 -> GlobRef.equal r1 r2 | PVar v1, PVar v2 -> Id.equal v1 v2 | PEvar (ev1, ctx1), PEvar (ev2, ctx2) -> Evar.equal ev1 ev2 && Array.equal constr_pattern_eq ctx1 ctx2 diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 9f0878578..dfbfb147f 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -8,12 +8,12 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open EConstr -open Globnames -open Glob_term +open Names open Mod_subst open Misctypes +open Glob_term open Pattern +open EConstr open Ltac_pretype (** {5 Functions on patterns} *) @@ -32,12 +32,12 @@ exception BoundPattern type [t] or raises [BoundPattern] (even if a sort); it raises an anomaly if [t] is an abstraction *) -val head_pattern_bound : constr_pattern -> global_reference +val head_pattern_bound : constr_pattern -> GlobRef.t (** [head_of_constr_reference c] assumes [r] denotes a reference and returns its label; raises an anomaly otherwise *) -val head_of_constr_reference : Evd.evar_map -> constr -> global_reference +val head_of_constr_reference : Evd.evar_map -> constr -> GlobRef.t (** [pattern_of_constr c] translates a term [c] with metavariables into a pattern; currently, no destructor (Cases, Fix, Cofix) and no diff --git a/pretyping/program.mli b/pretyping/program.mli index df0848ba1..a8f511578 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -8,37 +8,37 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open EConstr -open Globnames (** A bunch of Coq constants used by Progam *) -val sig_typ : unit -> global_reference -val sig_intro : unit -> global_reference -val sig_proj1 : unit -> global_reference -val sigT_typ : unit -> global_reference -val sigT_intro : unit -> global_reference -val sigT_proj1 : unit -> global_reference -val sigT_proj2 : unit -> global_reference +val sig_typ : unit -> GlobRef.t +val sig_intro : unit -> GlobRef.t +val sig_proj1 : unit -> GlobRef.t +val sigT_typ : unit -> GlobRef.t +val sigT_intro : unit -> GlobRef.t +val sigT_proj1 : unit -> GlobRef.t +val sigT_proj2 : unit -> GlobRef.t -val prod_typ : unit -> global_reference -val prod_intro : unit -> global_reference -val prod_proj1 : unit -> global_reference -val prod_proj2 : unit -> global_reference +val prod_typ : unit -> GlobRef.t +val prod_intro : unit -> GlobRef.t +val prod_proj1 : unit -> GlobRef.t +val prod_proj2 : unit -> GlobRef.t -val coq_eq_ind : unit -> global_reference -val coq_eq_refl : unit -> global_reference -val coq_eq_refl_ref : unit -> global_reference -val coq_eq_rect : unit -> global_reference +val coq_eq_ind : unit -> GlobRef.t +val coq_eq_refl : unit -> GlobRef.t +val coq_eq_refl_ref : unit -> GlobRef.t +val coq_eq_rect : unit -> GlobRef.t -val coq_JMeq_ind : unit -> global_reference -val coq_JMeq_refl : unit -> global_reference +val coq_JMeq_ind : unit -> GlobRef.t +val coq_JMeq_refl : unit -> GlobRef.t val mk_coq_and : Evd.evar_map -> constr list -> Evd.evar_map * constr val mk_coq_not : Evd.evar_map -> constr -> Evd.evar_map * constr (** Polymorphic application of delayed references *) -val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr +val papp : Evd.evar_map ref -> (unit -> GlobRef.t) -> constr array -> constr val get_proofs_transparency : unit -> bool val is_program_cases : unit -> bool diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index d070edead..84aceeedd 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -144,13 +144,13 @@ type obj_typ = { o_TCOMPS : constr list } (* ordered *) type cs_pattern = - Const_cs of global_reference + Const_cs of GlobRef.t | Prod_cs | Sort_cs of Sorts.family | Default_cs let eq_cs_pattern p1 p2 = match p1, p2 with -| Const_cs gr1, Const_cs gr2 -> eq_gr gr1 gr2 +| Const_cs gr1, Const_cs gr2 -> GlobRef.equal gr1 gr2 | Prod_cs, Prod_cs -> true | Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2 | Default_cs, Default_cs -> true diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 1f7b23c0c..748f053b2 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -10,7 +10,6 @@ open Names open Constr -open Globnames (** Operations concerning records and canonical structures *) @@ -40,10 +39,10 @@ val lookup_structure : inductive -> struc_typ val lookup_projections : inductive -> Constant.t option list (** raise [Not_found] if not a projection *) -val find_projection_nparams : global_reference -> int +val find_projection_nparams : GlobRef.t -> int (** raise [Not_found] if not a projection *) -val find_projection : global_reference -> struc_typ +val find_projection : GlobRef.t -> struc_typ (** {6 Canonical structures } *) (** A canonical structure declares "canonical" conversion hints between @@ -52,7 +51,7 @@ val find_projection : global_reference -> struc_typ (** A cs_pattern characterizes the form of a component of canonical structure *) type cs_pattern = - Const_cs of global_reference + Const_cs of GlobRef.t | Prod_cs | Sort_cs of Sorts.family | Default_cs @@ -71,9 +70,9 @@ val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * co val pr_cs_pattern : cs_pattern -> Pp.t -val lookup_canonical_conversion : (global_reference * cs_pattern) -> constr * obj_typ -val declare_canonical_structure : global_reference -> unit +val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ +val declare_canonical_structure : GlobRef.t -> unit val is_open_canonical_projection : Environ.env -> Evd.evar_map -> Reductionops.state -> bool val canonical_projections : unit -> - ((global_reference * cs_pattern) * obj_typ) list + ((GlobRef.t * cs_pattern) * obj_typ) list diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 244b8e60b..a4d447902 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -104,7 +104,7 @@ module ReductionBehaviour = struct type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ] type req = | ReqLocal - | ReqGlobal of global_reference * (int list * int * flag list) + | ReqGlobal of GlobRef.t * (int list * int * flag list) let load _ (_,(_,(r, b))) = table := Refmap.add r b !table diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index b8ac085a7..ad280d9f3 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -25,10 +25,10 @@ module ReductionBehaviour : sig (** [set is_local ref (recargs, nargs, flags)] *) val set : - bool -> Globnames.global_reference -> (int list * int * flag list) -> unit + bool -> GlobRef.t -> (int list * int * flag list) -> unit val get : - Globnames.global_reference -> (int list * int * flag list) option - val print : Globnames.global_reference -> Pp.t + GlobRef.t -> (int list * int * flag list) option + val print : GlobRef.t -> Pp.t end (** {6 Support for reduction effects } *) @@ -41,7 +41,7 @@ val declare_reduction_effect : effect_name -> (Environ.env -> Evd.evar_map -> Constr.constr -> unit) -> unit (* [set_reduction_effect cst name] declares effect [name] to be called when [cst] is found *) -val set_reduction_effect : Globnames.global_reference -> effect_name -> unit +val set_reduction_effect : GlobRef.t -> effect_name -> unit (* [effect_hook env sigma key term] apply effect associated to [key] on [term] *) val reduction_effect_hook : Environ.env -> Evd.evar_map -> Constr.constr -> diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 696001ab7..5a47acd22 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1279,7 +1279,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = error_cannot_recognize ref | _ -> try - if eq_gr (fst (global_of_constr sigma c)) ref + if GlobRef.equal (fst (global_of_constr sigma c)) ref then it_mkProd_or_LetIn t l else raise Not_found with Not_found -> diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index aa7604f53..e6065dda8 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -14,7 +14,6 @@ open Evd open EConstr open Reductionops open Pattern -open Globnames open Locus open Univ open Ltac_pretype @@ -30,13 +29,13 @@ exception ReductionTacticError of reduction_tactic_error val is_evaluable : Environ.env -> evaluable_global_reference -> bool -val error_not_evaluable : Globnames.global_reference -> 'a +val error_not_evaluable : GlobRef.t -> 'a val evaluable_of_global_reference : - Environ.env -> Globnames.global_reference -> evaluable_global_reference + Environ.env -> GlobRef.t -> evaluable_global_reference val global_of_evaluable_reference : - evaluable_global_reference -> Globnames.global_reference + evaluable_global_reference -> GlobRef.t exception Redelimination @@ -88,10 +87,10 @@ val reduce_to_quantified_ind : env -> evar_map -> types -> (inductive * EInstan (** [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form [t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *) val reduce_to_quantified_ref : - env -> evar_map -> global_reference -> types -> types + env -> evar_map -> GlobRef.t -> types -> types val reduce_to_atomic_ref : - env -> evar_map -> global_reference -> types -> types + env -> evar_map -> GlobRef.t -> types -> types val find_hnf_rectype : env -> evar_map -> types -> (inductive * EInstance.t) * constr list diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index e73a78fb8..4386144fe 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -71,10 +71,10 @@ type typeclass = { cl_univs : Univ.AUContext.t; (* The class implementation *) - cl_impl : global_reference; + cl_impl : GlobRef.t; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *) - cl_context : global_reference option list * Context.Rel.t; + cl_context : GlobRef.t option list * Context.Rel.t; (* Context of definitions and properties on defs, will not be shared *) cl_props : Context.Rel.t; @@ -91,12 +91,12 @@ type typeclass = { type typeclasses = typeclass Refmap.t type instance = { - is_class: global_reference; + is_class: GlobRef.t; is_info: hint_info_expr; (* Sections where the instance should be redeclared, None for discard, Some 0 for none. *) is_global: int option; - is_impl: global_reference; + is_impl: GlobRef.t; } type instances = (instance Refmap.t) Refmap.t @@ -480,7 +480,7 @@ let instances r = let cl = class_info r in instances_of cl let is_class gr = - Refmap.exists (fun _ v -> eq_gr v.cl_impl gr) !classes + Refmap.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes let is_instance = function | ConstRef c -> diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index e50d90b15..2a8e0b874 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -31,11 +31,11 @@ type typeclass = { (** The class implementation: a record parameterized by the context with defs in it or a definition if the class is a singleton. This acts as the class' global identifier. *) - cl_impl : global_reference; + cl_impl : GlobRef.t; (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The global reference gives a direct link to the class itself. *) - cl_context : global_reference option list * Context.Rel.t; + cl_context : GlobRef.t option list * Context.Rel.t; (** Context of definitions and properties on defs, will not be shared *) cl_props : Context.Rel.t; @@ -56,17 +56,17 @@ type typeclass = { type instance -val instances : global_reference -> instance list +val instances : GlobRef.t -> instance list val typeclasses : unit -> typeclass list val all_instances : unit -> instance list val add_class : typeclass -> unit -val new_instance : typeclass -> hint_info_expr -> bool -> global_reference -> instance +val new_instance : typeclass -> hint_info_expr -> bool -> GlobRef.t -> instance val add_instance : instance -> unit val remove_instance : instance -> unit -val class_info : global_reference -> typeclass (** raises a UserError if not a class *) +val class_info : GlobRef.t -> typeclass (** raises a UserError if not a class *) (** These raise a UserError if not a class. @@ -80,12 +80,12 @@ val typeclass_univ_instance : typeclass Univ.puniverses -> typeclass (** Just return None if not a class *) val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option -val instance_impl : instance -> global_reference +val instance_impl : instance -> GlobRef.t val hint_priority : instance -> int option -val is_class : global_reference -> bool -val is_instance : global_reference -> bool +val is_class : GlobRef.t -> bool +val is_instance : GlobRef.t -> bool (** Returns the term and type for the given instance of the parameters and fields of the type class. *) @@ -127,24 +127,24 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u val classes_transparent_state_hook : (unit -> transparent_state) Hook.t val classes_transparent_state : unit -> transparent_state -val add_instance_hint_hook : - (global_reference_or_constr -> global_reference list -> +val add_instance_hint_hook : + (global_reference_or_constr -> GlobRef.t list -> bool (* local? *) -> hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t -val remove_instance_hint_hook : (global_reference -> unit) Hook.t -val add_instance_hint : global_reference_or_constr -> global_reference list -> +val remove_instance_hint_hook : (GlobRef.t -> unit) Hook.t +val add_instance_hint : global_reference_or_constr -> GlobRef.t list -> bool -> hint_info_expr -> Decl_kinds.polymorphic -> unit -val remove_instance_hint : global_reference -> unit +val remove_instance_hint : GlobRef.t -> unit val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t -val declare_instance : hint_info_expr option -> bool -> global_reference -> unit +val declare_instance : hint_info_expr option -> bool -> GlobRef.t -> unit (** Build the subinstances hints for a given typeclass object. check tells if we should check for existence of the subinstances and add only the missing ones. *) -val build_subclasses : check:bool -> env -> evar_map -> global_reference -> +val build_subclasses : check:bool -> env -> evar_map -> GlobRef.t -> hint_info_expr -> - (global_reference list * hint_info_expr * constr) list + (GlobRef.t list * hint_info_expr * constr) list diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index e10c81c24..89c5d7e7b 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -9,17 +9,17 @@ (************************************************************************) (*i*) +open Names open EConstr open Environ open Constrexpr -open Globnames (*i*) type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr - | UnboundMethod of global_reference * Misctypes.lident (* Class name, method *) + | UnboundMethod of GlobRef.t * Misctypes.lident (* Class name, method *) | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (* found, expected *) exception TypeClassError of env * typeclass_error diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index d98295658..4aabc0aee 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -8,23 +8,23 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open EConstr open Environ open Constrexpr -open Globnames type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr - | UnboundMethod of global_reference * Misctypes.lident (** Class name, method *) + | UnboundMethod of GlobRef.t * Misctypes.lident (** Class name, method *) | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (** found, expected *) exception TypeClassError of env * typeclass_error val not_a_class : env -> constr -> 'a -val unbound_method : env -> global_reference -> Misctypes.lident -> 'a +val unbound_method : env -> GlobRef.t -> Misctypes.lident -> 'a val mismatched_ctx_inst : env -> contexts -> constr_expr list -> Context.Rel.t -> 'a diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 1f17d844f..b95691031 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -328,7 +328,7 @@ type 'a locatable_info = { type locatable = Locatable : 'a locatable_info -> locatable type logical_name = - | Term of global_reference + | Term of GlobRef.t | Dir of global_dir_reference | Syntactic of KerName.t | ModuleType of ModPath.t diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 213f0aeeb..2f2dcd563 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -12,7 +12,6 @@ open Names open Environ open Reductionops open Libnames -open Globnames open Misctypes open Evd @@ -50,7 +49,7 @@ val print_canonical_projections : env -> Evd.evar_map -> Pp.t (** Pretty-printing functions for type classes and instances *) val print_typeclasses : unit -> Pp.t -val print_instances : global_reference -> Pp.t +val print_instances : GlobRef.t -> Pp.t val print_all_instances : unit -> Pp.t val inspect : env -> Evd.evar_map -> int -> Pp.t diff --git a/printing/printer.mli b/printing/printer.mli index 41843680b..4af90e6a6 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Globnames open Constr open Environ open Pattern @@ -130,8 +129,8 @@ val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t (** Printing global references using names as short as possible *) -val pr_global_env : Id.Set.t -> global_reference -> Pp.t -val pr_global : global_reference -> Pp.t +val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t +val pr_global : GlobRef.t -> Pp.t val pr_constant : env -> Constant.t -> Pp.t val pr_existential_key : evar_map -> Evar.t -> Pp.t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 770d0940a..de96f8510 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -95,7 +95,7 @@ val pr_glls : goal list sigma -> Pp.t (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a - val pf_global : Id.t -> Proofview.Goal.t -> Globnames.global_reference + val pf_global : Id.t -> Proofview.Goal.t -> GlobRef.t (** FIXME: encapsulate the level in an existential type. *) val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 8e50c977e..8f50b0aa2 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -22,7 +22,7 @@ open Globnames let dnet_depth = ref 8 type term_label = -| GRLabel of global_reference +| GRLabel of GlobRef.t | ProdLabel | LambdaLabel | SortLabel diff --git a/tactics/hints.ml b/tactics/hints.ml index 739f1014a..d02bab186 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -115,7 +115,7 @@ type 'a hints_path_atom_gen = (* For forward hints, their names is the list of projections *) | PathAny -type hints_path_atom = global_reference hints_path_atom_gen +type hints_path_atom = GlobRef.t hints_path_atom_gen type 'a hints_path_gen = | PathAtom of 'a hints_path_atom_gen @@ -126,10 +126,10 @@ type 'a hints_path_gen = | PathEpsilon type pre_hints_path = Libnames.reference hints_path_gen -type hints_path = global_reference hints_path_gen +type hints_path = GlobRef.t hints_path_gen type hint_term = - | IsGlobRef of global_reference + | IsGlobRef of GlobRef.t | IsConstr of constr * Univ.ContextSet.t type 'a with_uid = { @@ -153,7 +153,7 @@ type 'a with_metadata = { type full_hint = hint with_metadata -type hint_entry = global_reference option * +type hint_entry = GlobRef.t option * raw_hint hint_ast with_uid with_metadata type import_level = [ `LAX | `WARN | `STRICT ] @@ -308,7 +308,7 @@ let instantiate_hint env sigma p = { p with code = { p.code with obj = code } } let hints_path_atom_eq h1 h2 = match h1, h2 with -| PathHints l1, PathHints l2 -> List.equal eq_gr l1 l2 +| PathHints l1, PathHints l2 -> List.equal GlobRef.equal l1 l2 | PathAny, PathAny -> true | _ -> false @@ -365,7 +365,7 @@ let path_seq p p' = let rec path_derivate hp hint = let rec derivate_atoms hints hints' = match hints, hints' with - | gr :: grs, gr' :: grs' when eq_gr gr gr' -> derivate_atoms grs grs' + | gr :: grs, gr' :: grs' when GlobRef.equal gr gr' -> derivate_atoms grs grs' | [], [] -> PathEpsilon | [], hints -> PathEmpty | grs, [] -> PathAtom (PathHints grs) @@ -474,28 +474,28 @@ module Hint_db : sig type t val empty : ?name:hint_db_name -> transparent_state -> bool -> t -val find : global_reference -> t -> search_entry +val find : GlobRef.t -> t -> search_entry val map_none : secvars:Id.Pred.t -> t -> full_hint list -val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list +val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list val map_existential : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list val map_eauto : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list val map_auto : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list val add_one : env -> evar_map -> hint_entry -> t -> t val add_list : env -> evar_map -> hint_entry list -> t -> t -val remove_one : global_reference -> t -> t -val remove_list : global_reference list -> t -> t -val iter : (global_reference option -> hint_mode array list -> full_hint list -> unit) -> t -> unit +val remove_one : GlobRef.t -> t -> t +val remove_list : GlobRef.t list -> t -> t +val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit val use_dn : t -> bool val transparent_state : t -> transparent_state val set_transparent_state : t -> transparent_state -> t val add_cut : hints_path -> t -> t -val add_mode : global_reference -> hint_mode array -> t -> t +val add_mode : GlobRef.t -> hint_mode array -> t -> t val cut : t -> hints_path val unfolds : t -> Id.Set.t * Cset.t -val fold : (global_reference option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> +val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a end = @@ -510,7 +510,7 @@ struct hintdb_map : search_entry Constr_map.t; (* A list of unindexed entries starting with an unfoldable constant or with no associated pattern. *) - hintdb_nopat : (global_reference option * stored_data) list; + hintdb_nopat : (GlobRef.t option * stored_data) list; hintdb_name : string option; } @@ -664,7 +664,7 @@ struct let remove_list grs db = let filter (_, h) = - match h.name with PathHints [gr] -> not (List.mem_f eq_gr gr grs) | _ -> true in + match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in { db with hintdb_map = hintmap; hintdb_nopat = hintnopat } @@ -1015,9 +1015,9 @@ type hint_action = | CreateDB of bool * transparent_state | AddTransparency of evaluable_global_reference list * bool | AddHints of hint_entry list - | RemoveHints of global_reference list + | RemoveHints of GlobRef.t list | AddCut of hints_path - | AddMode of global_reference * hint_mode array + | AddMode of GlobRef.t * hint_mode array let add_cut dbname path = let db = get_db dbname in @@ -1226,7 +1226,7 @@ type hints_entry = | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference list * bool - | HintsModeEntry of global_reference * hint_mode list + | HintsModeEntry of GlobRef.t * hint_mode list | HintsExternEntry of hint_info * Genarg.glob_generic_argument let default_prepare_hint_ident = Id.of_string "H" diff --git a/tactics/hints.mli b/tactics/hints.mli index b06ede0e1..c7de10a2a 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -12,7 +12,6 @@ open Util open Names open EConstr open Environ -open Globnames open Decl_kinds open Evd open Misctypes @@ -25,7 +24,7 @@ open Vernacexpr exception Bound -val decompose_app_bound : evar_map -> constr -> global_reference * constr array +val decompose_app_bound : evar_map -> constr -> GlobRef.t * constr array type debug = Debug | Info | Off @@ -51,7 +50,7 @@ type 'a hints_path_atom_gen = (* For forward hints, their names is the list of projections *) | PathAny -type hints_path_atom = global_reference hints_path_atom_gen +type hints_path_atom = GlobRef.t hints_path_atom_gen type hint_db_name = string type 'a with_metadata = private { @@ -81,7 +80,7 @@ type 'a hints_path_gen = | PathEpsilon type pre_hints_path = Libnames.reference hints_path_gen -type hints_path = global_reference hints_path_gen +type hints_path = GlobRef.t hints_path_gen val normalize_path : hints_path -> hints_path val path_matches : hints_path -> hints_path_atom list -> bool @@ -91,15 +90,15 @@ val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t val pp_hints_path : hints_path -> Pp.t val pp_hint_mode : hint_mode -> Pp.t val glob_hints_path_atom : - Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen + Libnames.reference hints_path_atom_gen -> GlobRef.t hints_path_atom_gen val glob_hints_path : - Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen + Libnames.reference hints_path_gen -> GlobRef.t hints_path_gen module Hint_db : sig type t val empty : ?name:hint_db_name -> transparent_state -> bool -> t - val find : global_reference -> t -> search_entry + val find : GlobRef.t -> t -> search_entry (** All hints which have no pattern. * [secvars] represent the set of section variables that @@ -107,27 +106,27 @@ module Hint_db : val map_none : secvars:Id.Pred.t -> t -> full_hint list (** All hints associated to the reference *) - val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list + val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments, _not_ using the discrimination net. *) val map_existential : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments and using the discrimination net. *) - val map_eauto : evar_map -> secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list + val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments. *) val map_auto : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list val add_one : env -> evar_map -> hint_entry -> t -> t val add_list : env -> evar_map -> hint_entry list -> t -> t - val remove_one : global_reference -> t -> t - val remove_list : global_reference list -> t -> t - val iter : (global_reference option -> + val remove_one : GlobRef.t -> t -> t + val remove_list : GlobRef.t list -> t -> t + val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit val use_dn : t -> bool @@ -147,7 +146,7 @@ type hnf = bool type hint_info = (patvar list * constr_pattern) Typeclasses.hint_info_gen type hint_term = - | IsGlobRef of global_reference + | IsGlobRef of GlobRef.t | IsConstr of constr * Univ.ContextSet.t type hints_entry = @@ -157,7 +156,7 @@ type hints_entry = | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference list * bool - | HintsModeEntry of global_reference * hint_mode list + | HintsModeEntry of GlobRef.t * hint_mode list | HintsExternEntry of hint_info * Genarg.glob_generic_argument val searchtable_map : hint_db_name -> hint_db @@ -171,7 +170,7 @@ val searchtable_add : (hint_db_name * hint_db) -> unit val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit -val remove_hints : bool -> hint_db_name list -> global_reference list -> unit +val remove_hints : bool -> hint_db_name list -> GlobRef.t list -> unit val current_db_names : unit -> String.Set.t @@ -264,7 +263,7 @@ val rewrite_db : hint_db_name val pr_searchtable : env -> evar_map -> Pp.t val pr_applicable_hint : unit -> Pp.t -val pr_hint_ref : env -> evar_map -> global_reference -> Pp.t +val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t val pr_hint_db : Hint_db.t -> Pp.t diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index b012a7ecd..b8f1ed720 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -294,13 +294,13 @@ let match_with_equation env sigma t = let (hdapp,args) = destApp sigma t in match EConstr.kind sigma hdapp with | Ind (ind,u) -> - if eq_gr (IndRef ind) glob_eq then + if GlobRef.equal (IndRef ind) glob_eq then Some (build_coq_eq_data()),hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if eq_gr (IndRef ind) glob_identity then + else if GlobRef.equal (IndRef ind) glob_identity then Some (build_coq_identity_data()),hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if eq_gr (IndRef ind) glob_jmeq then + else if GlobRef.equal (IndRef ind) glob_jmeq then Some (build_coq_jmeq_data()),hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) else diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 0697d0f19..f04cda123 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -144,7 +144,7 @@ val is_matching_sigma : Environ.env -> evar_map -> constr -> bool (** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns [t,u,T] and a boolean telling if equality is on the left side *) -val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr +val match_eqdec : Environ.env -> evar_map -> constr -> bool * GlobRef.t * constr * constr * constr (** Match a negation *) val is_matching_not : Environ.env -> evar_map -> constr -> bool diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index bc2f60186..cbaf691f1 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -135,7 +135,7 @@ val elimination_sort_of_hyp : Id.t -> goal sigma -> Sorts.family val elimination_sort_of_clause : Id.t option -> goal sigma -> Sorts.family val pf_with_evars : (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic -val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic +val pf_constr_of_global : GlobRef.t -> (constr -> tactic) -> tactic (** Tacticals defined directly in term of Proofview *) @@ -268,5 +268,5 @@ module New : sig val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic - val pf_constr_of_global : Globnames.global_reference -> constr Proofview.tactic + val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 59c035e83..ee76ad077 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3453,7 +3453,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma = type elim_scheme = { elimc: constr with_bindings option; elimt: types; - indref: global_reference option; + indref: GlobRef.t option; params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) nparams: int; (* number of parameters *) predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 7809dbf48..46f782eaa 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -16,7 +16,6 @@ open Proof_type open Evd open Clenv open Redexpr -open Globnames open Pattern open Unification open Misctypes @@ -177,7 +176,7 @@ val change : val pattern_option : (occurrences * constr) list -> goal_location -> unit Proofview.tactic val reduce : red_expr -> clause -> unit Proofview.tactic -val unfold_constr : global_reference -> unit Proofview.tactic +val unfold_constr : GlobRef.t -> unit Proofview.tactic (** {6 Modification of the local context. } *) @@ -253,7 +252,7 @@ val apply_delayed_in : type elim_scheme = { elimc: constr with_bindings option; elimt: types; - indref: global_reference option; + indref: GlobRef.t option; params: rel_context; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) nparams: int; (** number of parameters *) predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 753c608ad..611799990 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -37,7 +37,7 @@ struct type 't t = | DRel | DSort - | DRef of global_reference + | DRef of GlobRef.t | DCtx of 't * 't (* (binding list, subterm) = Prods and LetIns *) | DLambda of 't * 't | DApp of 't * 't (* binary app *) diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli index 7e13f8f28..0e2b0c80e 100644 --- a/vernac/assumptions.mli +++ b/vernac/assumptions.mli @@ -30,4 +30,4 @@ val traverse : {!traverse} also applies. *) val assumptions : ?add_opaque:bool -> ?add_transparent:bool -> transparent_state -> - global_reference -> constr -> types ContextObjectMap.t + GlobRef.t -> constr -> types ContextObjectMap.t diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 1a6b4dcdb..5e602289b 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -54,7 +54,7 @@ exception EqUnknown of string exception UndefinedCst of string exception InductiveWithProduct exception InductiveWithSort -exception ParameterWithoutEquality of global_reference +exception ParameterWithoutEquality of GlobRef.t exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported exception NoDecidabilityCoInductive @@ -635,7 +635,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). | App (c,ca) -> ( match EConstr.kind sigma c with | Ind (indeq, u) -> - if eq_gr (IndRef indeq) Coqlib.glob_eq + if GlobRef.equal (IndRef indeq) Coqlib.glob_eq then Tacticals.New.tclTHEN (do_replace_bl mode bl_scheme_key ind diff --git a/vernac/auto_ind_decl.mli b/vernac/auto_ind_decl.mli index 5cc783df7..11f26c7c3 100644 --- a/vernac/auto_ind_decl.mli +++ b/vernac/auto_ind_decl.mli @@ -23,7 +23,7 @@ exception EqUnknown of string exception UndefinedCst of string exception InductiveWithProduct exception InductiveWithSort -exception ParameterWithoutEquality of Globnames.global_reference +exception ParameterWithoutEquality of GlobRef.t exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported exception NoDecidabilityCoInductive diff --git a/vernac/class.ml b/vernac/class.ml index f0b01061b..06e1694f9 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -37,7 +37,7 @@ type coercion_error_kind = | ForbiddenSourceClass of cl_typ | NoTarget | WrongTarget of cl_typ * cl_typ - | NotAClass of global_reference + | NotAClass of GlobRef.t exception CoercionError of coercion_error_kind diff --git a/vernac/class.mli b/vernac/class.mli index 33d31fe1f..f7e837f3b 100644 --- a/vernac/class.mli +++ b/vernac/class.mli @@ -10,19 +10,18 @@ open Names open Classops -open Globnames (** Classes and coercions. *) (** [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion from [src] to [tg] *) -val try_add_new_coercion_with_target : global_reference -> local:bool -> +val try_add_new_coercion_with_target : GlobRef.t -> local:bool -> Decl_kinds.polymorphic -> source:cl_typ -> target:cl_typ -> unit (** [try_add_new_coercion ref s] declares [ref], assumed to be of type [(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *) -val try_add_new_coercion : global_reference -> local:bool -> +val try_add_new_coercion : GlobRef.t -> local:bool -> Decl_kinds.polymorphic -> unit (** [try_add_new_coercion_subclass cst s] expects that [cst] denotes a @@ -34,7 +33,7 @@ val try_add_new_coercion_subclass : cl_typ -> local:bool -> (** [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion from [src] to [tg] where the target is inferred from the type of [ref] *) -val try_add_new_coercion_with_source : global_reference -> local:bool -> +val try_add_new_coercion_with_source : GlobRef.t -> local:bool -> Decl_kinds.polymorphic -> source:cl_typ -> unit (** [try_add_new_identity_coercion id s src tg] enriches the @@ -47,4 +46,4 @@ val add_coercion_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook val add_subclass_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook -val class_of_global : global_reference -> cl_typ +val class_of_global : GlobRef.t -> cl_typ diff --git a/vernac/classes.mli b/vernac/classes.mli index e6134ee5d..27d3a4669 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -30,7 +30,7 @@ val declare_instance_constant : hint_info_expr -> (** priority *) bool -> (** globality *) Impargs.manual_explicitation list -> (** implicits *) - ?hook:(Globnames.global_reference -> unit) -> + ?hook:(GlobRef.t -> unit) -> Id.t -> (** name *) Univdecls.universe_decl -> bool -> (* polymorphic *) @@ -50,7 +50,7 @@ val new_instance : (bool * constr_expr) option -> ?generalize:bool -> ?tac:unit Proofview.tactic -> - ?hook:(Globnames.global_reference -> unit) -> + ?hook:(GlobRef.t -> unit) -> hint_info_expr -> Id.t diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index a2d20a1d1..2f2c7c4e2 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -11,7 +11,6 @@ open Names open Constr open Entries -open Globnames open Vernacexpr open Constrexpr open Decl_kinds @@ -33,4 +32,4 @@ val declare_assumption : coercion_flag -> assumption_kind -> types in_constant_universes_entry -> Universes.universe_binders -> Impargs.manual_implicits -> bool (** implicit *) -> Declaremods.inline -> variable CAst.t -> - global_reference * Univ.Instance.t * bool + GlobRef.t * Univ.Instance.t * bool diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 010874e23..12973f51b 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -8,17 +8,17 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Decl_kinds open Names +open Decl_kinds val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool val declare_definition : Id.t -> definition_kind -> Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits -> - Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference + GlobRef.t Lemmas.declaration_hook -> GlobRef.t val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Entries.constant_universes_entry -> Id.t -> Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> - Globnames.global_reference + GlobRef.t diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index aba5e32db..3d627d2f6 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -34,7 +34,7 @@ open Impargs module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a +type 'a declaration_hook = Decl_kinds.locality -> GlobRef.t -> 'a let mk_hook hook = hook let call_hook fix_exn hook l c = try hook l c diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index ad4c278e0..398f7d6d0 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -13,10 +13,10 @@ open Decl_kinds type 'a declaration_hook val mk_hook : - (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook + (Decl_kinds.locality -> GlobRef.t -> 'a) -> 'a declaration_hook val call_hook : - Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a + Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> GlobRef.t -> 'a (** A hook start_proof calls on the type of the definition being started *) val set_start_hook : (EConstr.types -> unit) -> unit diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 3f2792518..ae1065ef5 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -561,7 +561,7 @@ let declare_mutual_definition l = List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; let gr = List.hd kns in - let kn = match gr with ConstRef kn -> kn | _ -> assert false in + let kn = match gr with GlobRef.ConstRef kn -> kn | _ -> assert false in Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx; List.iter progmap_remove l; kn @@ -744,7 +744,7 @@ let all_programs () = type progress = | Remain of int | Dependent - | Defined of global_reference + | Defined of GlobRef.t let obligations_message rem = if rem > 0 then @@ -770,7 +770,7 @@ let update_obls prg obls rem = let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in if List.for_all (fun x -> obligations_solved x) progs then let kn = declare_mutual_definition progs in - Defined (ConstRef kn) + Defined (GlobRef.ConstRef kn) else Dependent) let is_defined obls x = not (Option.is_empty obls.(x).obl_body) @@ -891,7 +891,7 @@ let obligation_terminator name num guard hook auto pf = let obligation_hook prg obl num auto ctx' _ gr = let obls, rem = prg.prg_obligations in - let cst = match gr with ConstRef cst -> cst | _ -> assert false in + let cst = match gr with GlobRef.ConstRef cst -> cst | _ -> assert false in let transparent = evaluable_constant cst (Global.env ()) in let () = match obl.obl_status with (true, Evar_kinds.Expand) diff --git a/vernac/obligations.mli b/vernac/obligations.mli index cc2cacd86..4b6165fb1 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -12,7 +12,6 @@ open Environ open Constr open Evd open Names -open Globnames (* This is a hack to make it possible for Obligations to craft a Qed * behind the scenes. The fix_exn the Stm attaches to the Future proof @@ -49,7 +48,7 @@ type obligation_info = type progress = (* Resolution status of a program *) | Remain of int (* n obligations remaining *) | Dependent (* Dependent on other definitions *) - | Defined of global_reference (* Defined as id *) + | Defined of GlobRef.t (* Defined as id *) val default_tactic : unit Proofview.tactic ref diff --git a/vernac/record.mli b/vernac/record.mli index 992da2aa5..308c9e9b9 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -11,7 +11,6 @@ open Names open Vernacexpr open Constrexpr -open Globnames val primitive_flag : bool ref @@ -30,6 +29,6 @@ val definition_structure : inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic * Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * - Id.t * constr_expr option -> global_reference + Id.t * constr_expr option -> GlobRef.t -val declare_existing_class : global_reference -> unit +val declare_existing_class : GlobRef.t -> unit diff --git a/vernac/search.ml b/vernac/search.ml index a2a4fb40f..6d07187fe 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -22,8 +22,8 @@ open Nametab module NamedDecl = Context.Named.Declaration -type filter_function = global_reference -> env -> constr -> bool -type display_function = global_reference -> env -> constr -> unit +type filter_function = GlobRef.t -> env -> constr -> bool +type display_function = GlobRef.t -> env -> constr -> unit (* This option restricts the output of [SearchPattern ...], [SearchAbout ...], etc. to the names of the symbols matching the @@ -61,7 +61,7 @@ let iter_named_context_name_type f = List.iter (fun decl -> f (NamedDecl.get_id decl) (NamedDecl.get_type decl)) (* General search over hypothesis of a goal *) -let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) = +let iter_hypothesis glnum (fn : GlobRef.t -> env -> constr -> unit) = let env = Global.env () in let iter_hyp idh typ = fn (VarRef idh) env typ in let evmap,e = Pfedit.get_goal_context glnum in @@ -69,7 +69,7 @@ let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) = iter_named_context_name_type iter_hyp pfctxt (* General search over declarations *) -let iter_declarations (fn : global_reference -> env -> constr -> unit) = +let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = let env = Global.env () in let iter_obj (sp, kn) lobj = match object_tag lobj with | "VARIABLE" -> @@ -117,8 +117,7 @@ module ConstrPriority = struct (* The priority is memoised here. Because of the very localised use of this module, it is not worth it making a convenient interface. *) - type t = - Globnames.global_reference * Environ.env * Constr.t * priority + type t = GlobRef.t * Environ.env * Constr.t * priority and priority = int module ConstrSet = CSet.Make(Constr) diff --git a/vernac/search.mli b/vernac/search.mli index a1fb7ed3e..0dc82c1c3 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -12,7 +12,6 @@ open Names open Constr open Environ open Pattern -open Globnames (** {6 Search facilities. } *) @@ -20,8 +19,8 @@ type glob_search_about_item = | GlobSearchSubPattern of constr_pattern | GlobSearchString of string -type filter_function = global_reference -> env -> constr -> bool -type display_function = global_reference -> env -> constr -> unit +type filter_function = GlobRef.t -> env -> constr -> bool +type display_function = GlobRef.t -> env -> constr -> unit (** {6 Generic filter functions} *) |