diff options
author | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2016-04-15 16:45:14 +0200 |
---|---|---|
committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2016-04-15 16:45:14 +0200 |
commit | caa1f67de10614984fa7e1c68aa8adf0ff90196a (patch) | |
tree | 3c265ac5e16851c5dc1ca917ddb03725e09ea0ff /library/global.mli | |
parent | be824224cc76f729872e9d803fc64831b95aee94 (diff) | |
parent | 3b3d98acd58e91c960a2e11cd47ac19b2b34f86b (diff) |
Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh
Diffstat (limited to 'library/global.mli')
-rw-r--r-- | library/global.mli | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/library/global.mli b/library/global.mli index 363bb5789..bf653307c 100644 --- a/library/global.mli +++ b/library/global.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -19,9 +19,9 @@ val env : unit -> Environ.env val env_is_initial : unit -> bool -val universes : unit -> Univ.universes +val universes : unit -> UGraph.t val named_context_val : unit -> Environ.named_context_val -val named_context : unit -> Context.named_context +val named_context : unit -> Context.Named.t (** {6 Enriching the global environment } *) @@ -30,19 +30,20 @@ val set_engagement : Declarations.engagement -> unit (** Variables, Local definitions, constants, inductive types *) -val push_named_assum : (Id.t * Constr.types) Univ.in_universe_context_set -> unit -val push_named_def : (Id.t * Entries.definition_entry) -> unit +val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit +val push_named_def : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set val add_constant : - DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant + DirPath.t -> Id.t -> Safe_typing.global_declaration -> + constant * Safe_typing.exported_private_constant list val add_mind : DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive (** Extra universe constraints *) val add_constraints : Univ.constraints -> unit -val push_context : Univ.universe_context -> unit -val push_context_set : Univ.universe_context_set -> unit +val push_context : bool -> Univ.universe_context -> unit +val push_context_set : bool -> Univ.universe_context_set -> unit (** Non-interactive modules and module types *) @@ -72,7 +73,7 @@ val add_module_parameter : (** {6 Queries in the global environment } *) -val lookup_named : variable -> Context.named_declaration +val lookup_named : variable -> Context.Named.Declaration.t val lookup_constant : constant -> Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body |