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, 2 insertions, 1 deletions

diff --git a/library/lib.mli b/library/lib.mli
index f13ff82ae..570685585 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -88,6 +88,7 @@ val contents_after : object_name option -> library_segment
 (* User-side names *)
 val cwd : unit -> dir_path
 val make_path : identifier -> section_path
+val path_of_include : unit -> section_path
 
 (* Kernel-side names *)
 val current_prefix : unit -> module_path * dir_path
@@ -101,7 +102,7 @@ val sections_depth : unit -> int
 (* Are we inside an opened module type *)
 val is_modtype : unit -> bool
 val is_module : unit -> bool
-
+val current_mod_id : unit -> module_ident
 
 (* Returns the most recent OpenedThing node *)
 val what_is_opened : unit -> object_name * node