diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-19 18:21:04 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-19 18:21:04 +0000 |
| commit | 04dfb014ae67e1446aba386913131e18e6bbe41f (patch) | |
| tree | f36c281209313783b176473117f910f3818dd658 /kernel/declarations.ml | |
| parent | f0591d4fdf4a39c53ee690fc7285b592161406de (diff) | |
La notation 'with'. L'interpretation - version preliminaire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2975 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 8b1170597..05989bc82 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -148,7 +148,8 @@ and module_expr_body = | MEBapply of module_expr_body * module_expr_body * constraints -and module_specification_body = module_type_body * module_path option +and module_specification_body = + module_type_body * module_path option * constraints and structure_elem_body = | SEBconst of constant_body @@ -160,6 +161,7 @@ and module_structure_body = (label * structure_elem_body) list and module_body = { mod_expr : module_expr_body option; - mod_user_type : (module_type_body * constraints) option; + mod_user_type : module_type_body option; mod_type : module_type_body; - mod_equiv : module_path option } + mod_equiv : module_path option; + mod_constraints : constraints } |