Safe_typing code refactoring

 - No more modinfo sub-record in the safe_environment record,
   this was a syntactic pain.
     senv.modinfo.modpath --> senv.modpath
     senv.modinfo.variant --> senv.modvariant
     senv.modinfo.resolver --> senv.modresolver
     senv.modinfo.resolver_of_param --> senv.paramresolver
     senv.modinfo.label : removed (can be inferred from modpath)

 - No more systematic chaining of safe_environment ('old' field).
   Instead, earlier safe_environment is stored in the modvariant field
   when necessary (STRUCT and SIG case).

 - Improved sharing between end_module and end_modtype

 - More qualified names instead of open, better comments, ...

 - Some user errors are now checked earlier elsewhere (see for
   instance vernac_end_segment), so we can turn these errors into
   asserts. The user error about higher-order include is now algebraic.

 - Highlight the idea of a state monad in Safe_typing :
   type 'a safe_transformer = safe_environment -> 'a * safe_environment
   More systematic code in Global, thanks to 'globalize' function.

 - Declaremods : less informations stored in openmod_info

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16708 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 59 insertions, 62 deletions

diff --git a/library/global.mli b/library/global.mli
index a5ca92013..1bc745bb7 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -7,104 +7,101 @@
 (************************************************************************)
 
 open Names
-open Univ
-open Term
-open Context
-open Declarations
-open Entries
-open Indtypes
-open Mod_subst
-open Safe_typing
-
-(** This module defines the global environment of Coq.  The functions
+
+(** This module defines the global environment of Coq. The functions
    below are exactly the same as the ones in [Safe_typing], operating on
    that global environment. [add_*] functions perform name verification,
    i.e. check that the name given as argument match those provided by
    [Safe_typing]. *)
 
-
-
-val safe_env : unit -> safe_environment
+val safe_env : unit -> Safe_typing.safe_environment
 val env : unit -> Environ.env
 
-val env_is_empty : unit -> bool
+val env_is_initial : unit -> bool
 
-val universes : unit -> universes
+val universes : unit -> Univ.universes
 val named_context_val : unit -> Environ.named_context_val
 val named_context : unit -> Context.named_context
 
-val env_is_empty : unit -> bool
+(** {6 Enriching the global environment } *)
 
-(** {6 Extending env with variables and local definitions } *)
-val push_named_assum : (Id.t * types) -> Univ.constraints
-val push_named_def   : (Id.t * definition_entry) -> Univ.constraints
+(** Changing the (im)predicativity of the system *)
+val set_engagement : Declarations.engagement -> unit
 
-(** {6 ... } *)
-(** Adding constants, inductives, modules and module types.  All these
-  functions verify that given names match those generated by kernel *)
+(** Extra universe constraints *)
+val add_constraints : Univ.constraints -> unit
 
-val add_constant :
-  DirPath.t -> Id.t -> global_declaration -> constant
-val add_mind        :
-  DirPath.t -> Id.t -> mutual_inductive_entry -> mutual_inductive
-
-val add_module      :
- Id.t -> module_entry -> inline -> module_path * delta_resolver
-val add_modtype     :
- Id.t -> module_struct_entry -> inline -> module_path
-val add_include :
- module_struct_entry -> bool -> inline -> delta_resolver
+(** Variables, Local definitions, constants, inductive types *)
 
-val add_constraints : constraints -> unit
+val push_named_assum : (Id.t * Term.types) -> Univ.constraints
+val push_named_def   : (Id.t * Entries.definition_entry) -> Univ.constraints
+val add_constant :
+  DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant
+val add_mind :
+  DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive
 
-val set_engagement : engagement -> unit
+(** Non-interactive modules and module types *)
 
-(** {6 Interactive modules and module types }
-   Both [start_*] functions take the [DirPath.t] argument to create a
-   [mod_self_id]. This should be the name of the compilation unit. *)
+val add_module :
+  Id.t -> Entries.module_entry -> Declarations.inline ->
+    module_path * Mod_subst.delta_resolver
+val add_modtype :
+  Id.t -> Entries.module_struct_entry -> Declarations.inline -> module_path
+val add_include :
+  Entries.module_struct_entry -> bool -> Declarations.inline ->
+    Mod_subst.delta_resolver
 
-(** [start_*] functions return the [module_path] valid for components
-   of the started module / module type *)
+(** Interactive modules and module types *)
 
 val start_module : Id.t -> module_path
+val start_modtype : Id.t -> module_path
 
-val end_module : Summary.frozen ->Id.t ->
-  (module_struct_entry * inline) option -> module_path * delta_resolver
-
-val add_module_parameter :
- MBId.t -> module_struct_entry -> inline -> delta_resolver
+val end_module : Summary.frozen -> Id.t ->
+  (Entries.module_struct_entry * Declarations.inline) option ->
+    module_path * MBId.t list * Mod_subst.delta_resolver
 
-val start_modtype : Id.t -> module_path
-val end_modtype : Summary.frozen -> Id.t -> module_path
+val end_modtype : Summary.frozen -> Id.t -> module_path * MBId.t list
 
+val add_module_parameter :
+  MBId.t -> Entries.module_struct_entry -> Declarations.inline ->
+    Mod_subst.delta_resolver
+
+(** {6 Queries in the global environment } *)
+
+val lookup_named     : variable -> Context.named_declaration
+val lookup_constant  : constant -> Declarations.constant_body
+val lookup_inductive : inductive ->
+  Declarations.mutual_inductive_body * Declarations.one_inductive_body
+val lookup_mind      : mutual_inductive -> Declarations.mutual_inductive_body
+val lookup_module    : module_path -> Declarations.module_body
+val lookup_modtype   : module_path -> Declarations.module_type_body
+val exists_objlabel  : Label.t -> bool
 
-(** Queries *)
-val lookup_named     : variable -> named_declaration
-val lookup_constant  : constant -> constant_body
-val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body
-val lookup_mind      : mutual_inductive -> mutual_inductive_body
-val lookup_module    : module_path -> module_body
-val lookup_modtype   : module_path -> module_type_body
 val constant_of_delta_kn : kernel_name -> constant
 val mind_of_delta_kn : kernel_name -> mutual_inductive
-val exists_objlabel  : Label.t -> bool
 
-(** Compiled modules *)
+(** {6 Compiled libraries } *)
+
 val start_library : DirPath.t -> module_path
-val export : DirPath.t -> module_path * compiled_library * native_library
-val import : compiled_library -> Digest.t ->
+val export : DirPath.t ->
+  module_path * Safe_typing.compiled_library * Safe_typing.native_library
+val import : Safe_typing.compiled_library -> Digest.t ->
   module_path * Nativecode.symbol array
 
-(** {6 ... } *)
+(** {6 Misc } *)
+
 (** Function to get an environment from the constants part of the global
  * environment and a given context. *)
 
-val type_of_global : Globnames.global_reference -> types
+val type_of_global : Globnames.global_reference -> Term.types
 val env_of_context : Environ.named_context_val -> Environ.env
 
 val join_safe_environment : unit -> unit
 
-(** spiwack: register/unregister function for retroknowledge *)
-val register : Retroknowledge.field -> constr -> constr -> unit
+
+(** {6 Retroknowledge } *)
+
+val register :
+  Retroknowledge.field -> Term.constr -> Term.constr -> unit
 
 val register_inline : constant -> unit