diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-23 18:29:07 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-23 18:31:17 +0200 |
| commit | 1f11c1f1366b4c82e2e596b3cc97ee0052189741 (patch) | |
| tree | da1ad0cc24aea020f386d729b8dc8e0442537931 /stm/lemmas.ml | |
| parent | ee2adce57aac1ffe21681a9d31a8e8bc4f94210b (diff) | |
Fix for bug 1951, allowing at least fully-applied inductives types to be used
for building polymorphic instances of template polymorphic inductives.
Diffstat (limited to 'stm/lemmas.ml')
0 files changed, 0 insertions, 0 deletions