diff options
| author |  mlasson <marc.lasson@gmail.com> | 2015-06-22 21:14:20 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-07-09 11:41:55 +0200 |
| commit | 3a6b08286ac78c674d6d3e3073b38de26a610fdc (patch) | |
| tree | 112d68e4b412b9a096ba8e9fe62f0562fc43e5ac /library/library.ml | |
| parent | 1bf30962d7cd5732393d7722ae6d263d4c812ec8 (diff) | |
Template polymorphism: A bug-fix for Bug #4258
Reviewed by M. Sozeau
This commit fixes template polymorphism and makes it more precise,
applying to non-linear uses of the same universe in parameters of
template-polymorphic inductives. See bug report and
https://github.com/coq/coq/pull/69 for full details.
I also removed some deadcode in checker/inductive.ml.
I do not know if it is also necessary to fix checker/indtypes.ml.
Diffstat (limited to 'library/library.ml')
0 files changed, 0 insertions, 0 deletions