aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/topconstr.mli')
-rw-r--r--interp/topconstr.mli14
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 *)