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
---
 interp/topconstr.ml  | 5 ++++-
 interp/topconstr.mli | 5 ++++-
 2 files changed, 8 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 12ce52d1b5..a6b4b1b0ab 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1001,7 +1001,6 @@ type with_declaration_ast =
   | CWith_Module of identifier list located * qualid located
   | CWith_Definition of identifier list located * constr_expr
 
-
 type module_ast =
   | CMEident of qualid located
   | CMEapply of module_ast * module_ast
@@ -1015,6 +1014,10 @@ type include_ast =
   | CIMTE of module_type_ast * module_type_ast list
   | CIME of module_ast * module_ast list
 
+type 'a module_signature =
+  | Enforce of 'a (* ... : T *)
+  | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
+
 let loc_of_notation f loc (args,_) ntn =
   if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc)
   else snd (Util.unloc (f (List.hd args)))
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 1b6514a658..1c0b207eab 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -245,7 +245,6 @@ type with_declaration_ast =
   | CWith_Module of identifier list located * qualid located
   | CWith_Definition of identifier list located * constr_expr
 
-
 type module_ast =
   | CMEident of qualid located
   | CMEapply of module_ast * module_ast
@@ -259,5 +258,9 @@ type include_ast =
   | CIMTE of module_type_ast * module_type_ast list
   | CIME of module_ast * module_ast list
 
+type 'a module_signature =
+  | Enforce of 'a (* ... : T *)
+  | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
+
 val ntn_loc : Util.loc -> constr_expr notation_substitution -> string -> int
 val patntn_loc : Util.loc -> cases_pattern_expr notation_substitution -> string -> int
-- 
cgit v1.2.3