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, 14 insertions, 22 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 5f79c5363..d431fdfdd 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -54,15 +54,13 @@ type module_typing_error =
   | NoSuchLabel of Label.t
   | IncompatibleLabels of Label.t * Label.t
   | SignatureExpected of struct_expr_body
-  | NoModuleToEnd
-  | NoModuleTypeToEnd
   | NotAModule of string
   | NotAModuleType of string
   | NotAConstant of Label.t
   | IncorrectWithConstraint of Label.t
   | GenerativeModuleExpected of Label.t
-  | NonEmptyLocalContect of Label.t option
   | LabelMissing of Label.t * string
+  | HigherOrderInclude
 
 exception ModuleTypingError of module_typing_error
 
@@ -93,12 +91,6 @@ let error_incompatible_labels l l' =
 let error_signature_expected mtb =
   raise (ModuleTypingError (SignatureExpected mtb))
 
-let error_no_module_to_end _ =
-  raise (ModuleTypingError NoModuleToEnd)
-
-let error_no_modtype_to_end _ =
-  raise (ModuleTypingError NoModuleTypeToEnd)
-
 let error_not_a_module s =
   raise (ModuleTypingError (NotAModule s))
 
@@ -111,13 +103,11 @@ let error_incorrect_with_constraint l =
 let error_generative_module_expected l =
   raise (ModuleTypingError (GenerativeModuleExpected l))
 
-let error_non_empty_local_context lo =
-  raise (ModuleTypingError (NonEmptyLocalContect lo))
-
 let error_no_such_label_sub l l1 =
   raise (ModuleTypingError (LabelMissing (l,l1)))
 
-(************************)
+let error_higher_order_include () =
+  raise (ModuleTypingError HigherOrderInclude)
 
 let destr_functor mtb =
   match mtb with
@@ -267,19 +257,21 @@ let rec add_signature mp sign resolver env =
       | SFBmind mib ->
 	Environ.add_mind (mind_of_delta_kn resolver kn) mib env
       | SFBmodule mb -> add_module mb env (* adds components as well *)
-      | SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env
+      | SFBmodtype mtb -> Environ.add_modtype mtb env
   in
     List.fold_left add_one env sign
 
-and add_module mb env = 
+and add_module mb env =
   let mp = mb.mod_mp in
-  let env = Environ.shallow_add_module mp mb env in
-    match mb.mod_type with
-      | SEBstruct (sign) -> 
-	  add_retroknowledge mp mb.mod_retroknowledge 
-	    (add_signature mp sign mb.mod_delta env)
-      | SEBfunctor _ -> env
-      | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
+  let env = Environ.shallow_add_module mb env in
+  match mb.mod_type with
+  | SEBstruct (sign) ->
+    add_retroknowledge mp mb.mod_retroknowledge
+      (add_signature mp sign mb.mod_delta env)
+  | SEBfunctor _ -> env
+  | _ ->
+    anomaly ~label:"Modops"
+      (Pp.str "the evaluation of the structure failed ")
 
 let strengthen_const mp_from l cb resolver =
   match cb.const_body with