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/entries.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/entries.ml')
| -rw-r--r-- | kernel/entries.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 4d86d6d2c..edba6e608 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -78,10 +78,13 @@ and module_type_entry = MTEident of kernel_name | MTEfunsig of mod_bound_id * module_type_entry * module_type_entry | MTEsig of mod_self_id * module_signature_entry + | MTEwith of module_type_entry * with_declaration and module_signature_entry = (label * specification_entry) list - +and with_declaration = + With_Module of identifier * module_path + | With_Definition of identifier * constr and module_expr = MEident of module_path |