diff options
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/library/global.mli b/library/global.mli index b82039a0..2819c187 100644 --- a/library/global.mli +++ b/library/global.mli @@ -23,13 +23,14 @@ val env_is_initial : unit -> bool val universes : unit -> UGraph.t val named_context_val : unit -> Environ.named_context_val -val named_context : unit -> Context.Named.t +val named_context : unit -> Constr.named_context (** {6 Enriching the global environment } *) (** Changing the (im)predicativity of the system *) val set_engagement : Declarations.engagement -> unit val set_typing_flags : Declarations.typing_flags -> unit +val typing_flags : unit -> Declarations.typing_flags (** Variables, Local definitions, constants, inductive types *) @@ -79,7 +80,7 @@ val add_module_parameter : (** {6 Queries in the global environment } *) -val lookup_named : variable -> Context.Named.Declaration.t +val lookup_named : variable -> Constr.named_declaration val lookup_constant : Constant.t -> Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body @@ -123,26 +124,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 } *) @@ -155,6 +156,8 @@ val register_inline : Constant.t -> unit val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit +val set_reduction_sharing : bool -> unit + (* Modifies the global state, registering new universes *) val current_modpath : unit -> ModPath.t |