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

3 files changed, 14 insertions, 15 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
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
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index 97ab9efc88..9ba1d6715c 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -1617,14 +1617,13 @@ let xlate_module_binder_list (l:module_binder list) =
 		 CT_module_binder
 		   (CT_id_ne_list(fst, idl2), xlate_module_type mty)) l);;
 
-let xlate_module_type_check_opt = function
-    None -> CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK
- 	(CT_coerce_ID_OPT_to_MODULE_TYPE_OPT ctv_ID_OPT_NONE)
-  | Some(mty, true) -> CT_only_check(xlate_module_type mty)
-  | Some(mty, false) ->
+let xlate_module_type_check = function
+  | Topconstr.Enforce mty ->
       CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK
 	(CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT
-	   (xlate_module_type mty));;
+	   (xlate_module_type mty))
+  | Topconstr.Check mtys ->
+      CT_only_check (List.map xlate_module_type mtys)
 
 let rec xlate_module_expr = function
     CMEident (_, qid) -> CT_coerce_ID_OPT_to_MODULE_EXPR
@@ -2034,7 +2033,7 @@ let rec xlate_vernac =
        xlate_error"TODO: Local abbreviations and abbreviations with parameters"
   (* Modules and Module Types *)
    | VernacInclude (_) -> xlate_error "TODO : Include "
-   | VernacDeclareModuleType((_, id), bl, mty_o)  ->
+   | VernacDeclareModuleType((_, id), bl, _, mty_o)  ->
       CT_module_type_decl(xlate_ident id,
 			  xlate_module_binder_list bl,
 			  match mty_o with
@@ -2045,18 +2044,18 @@ let rec xlate_vernac =
 				CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT
 				  (xlate_module_type mty1)
 	                    | _ -> failwith "TODO: Include Self")
-   | VernacDefineModule(_,(_, id), bl, mty_o, mexpr_o) ->
+   | VernacDefineModule(_,(_, id), bl, mtys, mexpr_o) ->
        CT_module(xlate_ident id,
 		 xlate_module_binder_list bl,
-		 xlate_module_type_check_opt mty_o,
+		 xlate_module_type_check mtys,
 		 match mexpr_o with
 		     [] -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE
 		   | [m] -> xlate_module_expr m
 		   | _ -> failwith "TODO Include Self")
-  | VernacDeclareModule(_,(_, id), bl, mty_o) ->
+  | VernacDeclareModule(_,(_, id), bl, mty) ->
        CT_declare_module(xlate_ident id,
 		 xlate_module_binder_list bl,
-		 xlate_module_type_check_opt (Some mty_o),
+		 xlate_module_type_check (Topconstr.Enforce mty),
 		 CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE)
    | VernacRequire (impexp, spec, id::idl) ->
       let ct_impexp, ct_spec = get_require_flags impexp spec in