diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-07 15:32:49 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-07 15:32:49 +0000 |
| commit | 9b6517c0c933fb1d66c7feb53fa57e1697d8124a (patch) | |
| tree | d914d6bc2c5598baad03807ce40ada0b1d56045d /interp/topconstr.mli | |
| parent | e3e6ff629e258269bc9fe06f7be99a2d5f334071 (diff) | |
Include can accept both Module and Module Type
Syntax Include Type is still active, but deprecated, and triggers a warning.
The syntax M <+ M' <+ M'', which performs internally an Include, also
benefits from this: M, M', M'' can be independantly modules or module type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12640 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/topconstr.mli')
| -rw-r--r-- | interp/topconstr.mli | 14 |
1 files changed, 3 insertions, 11 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 6e3951b2f..1b1698f95 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -242,17 +242,9 @@ type with_declaration_ast = | CWith_Definition of identifier list located * constr_expr type module_ast = - | CMEident of qualid located - | CMEapply of module_ast * module_ast - -type module_type_ast = - | CMTEident of qualid located - | CMTEapply of module_type_ast * module_ast - | CMTEwith of module_type_ast * with_declaration_ast - -type include_ast = - | CIMTE of module_type_ast list - | CIME of module_ast list + | CMident of qualid located + | CMapply of module_ast * module_ast + | CMwith of module_ast * with_declaration_ast type 'a module_signature = | Enforce of 'a (* ... : T *) |