diff options
| author |  soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-14 11:27:37 +0000 |
|---|---|---|
| committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-14 11:27:37 +0000 |
| commit | 0d0d1ba857ed4aa70e3da24209e61dfa8122d0d9 (patch) | |
| tree | 87075a220561a38e0d453a6b0e3b5659ef46dd2c /kernel/declarations.ml | |
| parent | 86b114cf4d7beb1cbf8b3e205acc245e84ca47e8 (diff) | |
Ajout des alias de module dans le noyau.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10664 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 63c690d48..475ef042d 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -251,13 +251,14 @@ type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBmodtype of struct_expr_body + | SFBalias of module_path * constraints option + | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list and struct_expr_body = | SEBident of module_path - | SEBfunctor of mod_bound_id * struct_expr_body * struct_expr_body + | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body | SEBstruct of mod_self_id * structure_body | SEBapply of struct_expr_body * struct_expr_body * constraints @@ -270,8 +271,11 @@ and with_declaration_body = and module_body = { mod_expr : struct_expr_body option; mod_type : struct_expr_body option; - mod_equiv : module_path option; mod_constraints : constraints; + mod_alias : substitution; mod_retroknowledge : Retroknowledge.action list} -type module_type_body = struct_expr_body * module_path option +and module_type_body = + { typ_expr : struct_expr_body; + typ_strength : module_path option; + typ_alias : substitution} |