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/ascent.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/interface/ascent.mli')

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