diff options
| author |  soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-15 15:07:10 +0000 |
|---|---|---|
| committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-15 15:07:10 +0000 |
| commit | d1df4f36c4e304d6ed446d09b64d1b3bf34bac16 (patch) | |
| tree | 957ac29812b949cc7aee31e4dae187fec02b31d5 /checker/declarations.mli | |
| parent | e9d5db3172cd707288166d3bf31506881ff1c16e (diff) | |
Report des commits 11417 et 11437 de la v8.2
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11454 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/declarations.mli')
| -rw-r--r-- | checker/declarations.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/checker/declarations.mli b/checker/declarations.mli index fdea3383b..225f91604 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -150,7 +150,7 @@ type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBalias of module_path * Univ.constraints option + | SFBalias of module_path * struct_expr_body option * Univ.constraints option | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list @@ -164,7 +164,8 @@ and struct_expr_body = | SEBwith of struct_expr_body * with_declaration_body and with_declaration_body = - With_module_body of identifier list * module_path * Univ.constraints + With_module_body of identifier list * module_path * + struct_expr_body option * Univ.constraints | With_definition_body of identifier list * constant_body and module_body = |