diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-01-06 13:04:36 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-01-06 13:04:36 +0000 |
| commit | fe570f948ce85c300a3677fe600215d2924905cb (patch) | |
| tree | b4864895bfe9be3a05ed1e670610512338570f1d /library/declaremods.mli | |
| parent | 842c86fd96b02b757cf47f57f4eb888fe40e10f4 (diff) | |
- 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
Diffstat (limited to 'library/declaremods.mli')
| -rw-r--r-- | library/declaremods.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/library/declaremods.mli b/library/declaremods.mli index be9953f43..17a97e7ae 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -43,9 +43,8 @@ val declare_module : 'modexpr option -> unit val start_module : (env -> 'modtype -> module_type_entry) -> - identifier -> - (identifier located list * 'modtype) list -> ('modtype * bool) option -> - unit + bool option -> identifier -> (identifier located list * 'modtype) list -> + ('modtype * bool) option -> unit val end_module : identifier -> unit |