diff options
| author | letouzey | 2009-11-18 00:03:14 +0000 |
|---|---|---|
| committer | letouzey | 2009-11-18 00:03:14 +0000 |
| commit | 2ddd0afea124874576b1468c3ce5830352be4322 (patch) | |
| tree | 5e49b6d68d695e89c861a13f860d76916c544051 /plugins/interface/ascent.mli | |
| parent | df89fbc8ac8d0d485c1a373cb4edbb1835e2c4ad (diff) | |
Module subtyping : allow many <: and module type declaration with <:
Any place where <: was legal can now contain many <: declarations.
Moreover we can say that the module type we are declaring is a subtype
of an earlier module type. See DecidableType2 for examples.
Also try to handle correctly the freeze/unfreeze summaries
when simulating start/include/end (syntax ... := ... <+ ...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12532 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/interface/ascent.mli')
| -rw-r--r-- | plugins/interface/ascent.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/interface/ascent.mli b/plugins/interface/ascent.mli index bc615f14ec..bd82688d33 100644 --- a/plugins/interface/ascent.mli +++ b/plugins/interface/ascent.mli @@ -479,7 +479,7 @@ and ct_MODULE_TYPE = | CT_module_type_with_mod of ct_MODULE_TYPE * ct_ID_LIST * ct_ID and ct_MODULE_TYPE_CHECK = CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK of ct_MODULE_TYPE_OPT - | CT_only_check of ct_MODULE_TYPE + | CT_only_check of ct_MODULE_TYPE list and ct_MODULE_TYPE_OPT = CT_coerce_ID_OPT_to_MODULE_TYPE_OPT of ct_ID_OPT | CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT of ct_MODULE_TYPE |