diff options
| author | herbelin | 2011-03-05 16:42:38 +0000 |
|---|---|---|
| committer | herbelin | 2011-03-05 16:42:38 +0000 |
| commit | 0c2dd4a32538ebda7c964c249f158054b6cc2e1a (patch) | |
| tree | 86748aeff7f6a18ee4853af8945beb10343f7855 /interp/modintern.ml | |
| parent | 8cff4906c3e6149063a6a6c9c570b1a54775dcc8 (diff) | |
Starting being more explicit on the reasons why module subtyping fails.
Note: I'm unsure about some subtyping error case apparently involving
aliases of inductive types (middle of Subtyping.check_inductive); I
bound it to some NotEqualInductiveAliases error, but this has to be
checked.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13885 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/modintern.ml')
0 files changed, 0 insertions, 0 deletions