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

diff --git a/library/lib.ml b/library/lib.ml
index 8fff32e1a..de2047dbd 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -98,11 +98,15 @@ let library_dp () =
    module path and relative section path *)
 let path_prefix = ref initial_prefix
 
-
 let cwd () = fst !path_prefix
 
 let make_path id = Libnames.make_path (cwd ()) id
 
+let path_of_include () =
+  let dir = Names.repr_dirpath (cwd ()) in
+  let new_dir = List.tl dir in
+  let id = List.hd dir in
+    Libnames.make_path (Names.make_dirpath new_dir) id
 
 let current_prefix () = snd !path_prefix
 
@@ -236,12 +240,25 @@ let add_frozen_state () =
 
 (* Modules. *)
 
+
 let is_something_opened = function 
     (_,OpenedSection _) -> true 
   | (_,OpenedModule _) -> true
   | (_,OpenedModtype _) -> true
   | _ -> false
 
+
+let current_mod_id () = 
+  try match find_entry_p is_something_opened with
+    | oname,OpenedModule (_,_,nametab) -> 
+	basename (fst oname)
+    | oname,OpenedModtype (_,nametab) -> 
+	basename (fst oname)
+    | _ -> error "you are not in a module"
+  with Not_found ->
+    error "no opened modules"
+
+
 let start_module export id mp nametab = 
   let dir = extend_dirpath (fst !path_prefix) id in
   let prefix = dir,(mp,empty_dirpath) in
@@ -586,7 +603,8 @@ let reset_name (loc,id) =
 let is_mod_node = function 
   | OpenedModule _ | OpenedModtype _ | OpenedSection _ 
   | ClosedModule _ | ClosedModtype _ | ClosedSection _  -> true 
-  | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE"
+  | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE" 
+	|| t = "MODULE ALIAS"
   | _ -> false
 
 (* Reset on a module or section name in order to bypass constants with