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