From fe570f948ce85c300a3677fe600215d2924905cb Mon Sep 17 00:00:00 2001 From: sacerdot Date: Thu, 6 Jan 2005 13:04:36 +0000 Subject: - Module/Declare Module syntax made more uniform: * "Module X [binders] [:T] [:= b]." is now used to define a module both in module definitions and module type definitions. Moreover "b" can now be a functor application in every situation (this was not accepted for module definitions in module type definitions) * "Declare Module X : T." is now used to declare a module both in module definitions and module type definitions. - Added syntactic sugar "Declare Module Export/Import" and "Module Export/Import" - Added syntactic sugar "Module M(Export/Import X Y: T)" and "Module Type M(Export/Import X Y: T)" (only for interactive definitions) (doc TODO) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6564 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/lib.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'library/lib.ml') diff --git a/library/lib.ml b/library/lib.ml index 16521e627..980fd7e4c 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -21,7 +21,7 @@ open Summary type node = | Leaf of obj | CompilingLibrary of object_prefix - | OpenedModule of object_prefix * Summary.frozen + | OpenedModule of bool option * object_prefix * Summary.frozen | OpenedModtype of object_prefix * Summary.frozen | OpenedSection of object_prefix * Summary.frozen (* bool is to tell if the section must be opened automatically *) @@ -125,7 +125,7 @@ let sections_are_opened () = let recalc_path_prefix () = let rec recalc = function | (sp, OpenedSection (dir,_)) :: _ -> dir - | (sp, OpenedModule (dir,_)) :: _ -> dir + | (sp, OpenedModule (_,dir,_)) :: _ -> dir | (sp, OpenedModtype (dir,_)) :: _ -> dir | (sp, CompilingLibrary dir) :: _ -> dir | _::l -> recalc l @@ -231,13 +231,13 @@ let export_segment seg = clean [] seg -let start_module id mp nametab = +let start_module export id mp nametab = let dir = extend_dirpath (fst !path_prefix) id in let prefix = dir,(mp,empty_dirpath) in let oname = make_path id, make_kn id in if Nametab.exists_module dir then errorlabstrm "open_module" (pr_id id ++ str " already exists") ; - add_entry oname (OpenedModule (prefix,nametab)); + add_entry oname (OpenedModule (export,prefix,nametab)); path_prefix := prefix; prefix (* add_frozen_state () must be called in declaremods *) @@ -245,7 +245,7 @@ let start_module id mp nametab = let end_module id = let oname,nametab = try match find_entry_p is_something_opened with - | oname,OpenedModule (_,nametab) -> + | oname,OpenedModule (_,_,nametab) -> let sp = fst oname in let id' = basename sp in if id<>id' then error "this is not the last opened module"; -- cgit v1.2.3