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 /plugins/xml | |
| 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 'plugins/xml')
0 files changed, 0 insertions, 0 deletions