diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-01 09:12:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-01 09:12:05 +0000 |
| commit | 8ce32469bc02e2ecf3f1dfee56f960f19412de9b (patch) | |
| tree | 5c362d622ef2eb901ad8bdf6b6f865263294a742 /theories | |
| parent | 0e4c44431739bd607f3eb95d6287ea35b4613e5d (diff) | |
Fixing critical part of bug #2504. Not all inductive types in Type are
polymorphic and only for inductive polymorphic types is the conclusion
of the arity irrelevant. Refreshing at discharge time (that
indtypes.ml expects for retyping) should be done only for polymorphic
types. For monomorphic inductive types in Type, the type level is
possibly related to universe constraints stored in the section and it
must not be changed. [Alternatively, discharge should not retype
inductive types from scratch, but instead generalize them over the
section variables, the same way it does for definitions/axioms. But
that's another story.]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14501 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
0 files changed, 0 insertions, 0 deletions