From 2ddd0afea124874576b1468c3ce5830352be4322 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 18 Nov 2009 00:03:14 +0000
Subject: 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
---
 plugins/interface/vtp.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/interface/vtp.ml')

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
-- 
cgit v1.2.3