diff options
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/library/global.mli b/library/global.mli index 007986d1..278b9e65 100644 --- a/library/global.mli +++ b/library/global.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: global.mli,v 1.40.2.2 2005/11/23 14:46:17 barras Exp $ i*) +(*i $Id: global.mli 7899 2006-01-20 16:35:03Z barras $ i*) (*i*) open Names @@ -29,7 +29,10 @@ open Safe_typing val safe_env : unit -> safe_environment val env : unit -> Environ.env +val env_is_empty : unit -> bool + val universes : unit -> universes +val named_context_val : unit -> Environ.named_context_val val named_context : unit -> Sign.named_context val env_is_empty : unit -> bool @@ -42,7 +45,7 @@ val push_named_def : (identifier * constr * types option) -> Univ.constraints functions verify that given names match those generated by kernel *) val add_constant : - dir_path -> identifier -> global_declaration -> kernel_name + dir_path -> identifier -> global_declaration -> constant val add_mind : dir_path -> identifier -> mutual_inductive_entry -> kernel_name @@ -51,7 +54,7 @@ val add_modtype : identifier -> module_type_entry -> kernel_name val add_constraints : constraints -> unit -val set_engagement : Environ.engagement -> unit +val set_engagement : engagement -> unit (*s Interactive modules and module types *) (* Both [start_*] functions take the [dir_path] argument to create a @@ -93,5 +96,5 @@ val import : compiled_library -> Digest.t -> module_path * environment and a given context. *) val type_of_global : Libnames.global_reference -> types -val env_of_context : Sign.named_context -> Environ.env +val env_of_context : Environ.named_context_val -> Environ.env |