Beaoucoup de changements dans la representation interne des modules.

kernel:

-declaration.ml
   unification des representations pour les modules et modules types.
     (type struct_expr_body)

-mod_typing.ml
   le typage des modules est separe de l'evaluation des modules

-modops.ml
   nouvelle fonction qui pour toutes expressions de structure calcule
   sa forme evaluee.(eval_struct)

-safe_typing.ml
  ajout du support du nouvel operateur Include.(add_include).


library:

-declaremods.ml
   nouveaux objets Include et Module-alias et gestion de la resolution de noms pour
   les alias via la nametab.

parsing:

-g_vernac.ml4:
   nouvelles regles pour le support des Includes et pour l'application des signatures
   fonctorielles.


extraction:
  Adaptation a la nouvelle representation des modules et support de l'operateur with.




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

1 files changed, 6 insertions, 2 deletions

diff --git a/interp/modintern.mli b/interp/modintern.mli
index a8676c793..1f27e3c18 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -12,13 +12,17 @@
 open Declarations
 open Environ
 open Entries
+open Util
+open Libnames
+open Names
 open Topconstr
 (*i*)
 
 (* Module expressions and module types are interpreted relatively to 
    eventual functor or funsig arguments. *)
 
-val interp_modtype : env -> module_type_ast -> module_type_entry
+val interp_modtype : env -> module_type_ast -> module_struct_entry
 
-val interp_modexpr : env -> module_ast -> module_expr
+val interp_modexpr : env -> module_ast -> module_struct_entry
 
+val lookup_module : qualid located -> module_path