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/vtp.ml | |
| 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/vtp.ml')
| -rw-r--r-- | plugins/interface/vtp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/interface/vtp.ml b/plugins/interface/vtp.ml index a84f9ea56a..d713361509 100644 --- a/plugins/interface/vtp.ml +++ b/plugins/interface/vtp.ml @@ -1185,9 +1185,9 @@ and fMODULE_TYPE = function fNODE "module_type_with_mod" 3 and fMODULE_TYPE_CHECK = function | CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK x -> fMODULE_TYPE_OPT x -| CT_only_check(x1) -> - fMODULE_TYPE x1 ++ - fNODE "only_check" 1 +| CT_only_check(l) -> + (List.fold_left (++) (mt()) (List.map fMODULE_TYPE l)) ++ + fNODE "only_check" (List.length l) and fMODULE_TYPE_OPT = function | CT_coerce_ID_OPT_to_MODULE_TYPE_OPT x -> fID_OPT x | CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT x -> fMODULE_TYPE x |