diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-05 15:51:57 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-05 15:51:57 +0000 |
| commit | 8082d1faf85a0ab29f6c144a137791902a4e9c1f (patch) | |
| tree | 431f9fc4fe167e77c6be5163db41314ecd872ba6 /kernel/mod_subst.mli | |
| parent | b82f23627766b39ca0343ac41b061a5ce76c18f2 (diff) | |
Fixing critical inductive polymorphism bug found by Bruno.
If two distinct parameters of the inductive type contributes to
polymorphism, they must have distinct names, othewise an aliasing
problem of the form "fun x x => max(x,x)" happens.
Also insisted that a parameter contributes to universe polymorphism
only if the corresponding occurrence of Type is not hidden behind a
definition.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14511 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/mod_subst.mli')
0 files changed, 0 insertions, 0 deletions