diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-09-20 10:53:18 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-09-20 10:53:18 +0000 |
| commit | dc16cbc0693d98c324c846e162d087d95d60f70d (patch) | |
| tree | dd0d0ab7e38f8d8334827a3711fd62acbd1cd18c /library/declaremods.mli | |
| parent | a406d5f7602f44daf8066faf399acbad3ba124fc (diff) | |
La notation with dependante + affichage dependante de moduels corrige
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3025 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declaremods.mli')
| -rw-r--r-- | library/declaremods.mli | 21 |
1 files changed, 16 insertions, 5 deletions
diff --git a/library/declaremods.mli b/library/declaremods.mli index 17db827e8..5c228d161 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -11,6 +11,7 @@ (*i*) open Names open Entries +open Environ open Libnames open Libobject open Lib @@ -22,22 +23,32 @@ open Lib (*s Modules *) -val declare_module : identifier -> module_entry -> unit +val declare_module : + (env -> 'modtype -> module_type_entry) -> (env -> 'modexpr -> module_expr) -> + identifier -> + (identifier list * 'modtype) list -> 'modtype option -> 'modexpr option -> unit + +val start_module : (env -> 'modtype -> module_type_entry) -> + identifier -> (identifier list * 'modtype) list -> 'modtype option -> unit + +(*val declare_module : identifier -> module_entry -> unit val start_module : identifier -> identifier list -> (mod_bound_id * module_type_entry) list -> module_type_entry option -> unit +*) val end_module : identifier -> unit (*s Module types *) -val declare_modtype : identifier -> module_type_entry -> unit +val declare_modtype : (env -> 'modtype -> module_type_entry) -> + identifier -> (identifier list * 'modtype) list -> 'modtype -> unit + +val start_modtype : (env -> 'modtype -> module_type_entry) -> + identifier -> (identifier list * 'modtype) list -> unit -val start_modtype : - identifier -> identifier list -> (mod_bound_id * module_type_entry) list - -> unit val end_modtype : identifier -> unit |