diff options
| author | Maxime Dénès | 2014-07-30 21:32:55 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-07-31 01:08:33 -0400 |
| commit | 72d3f73a4a4596558e06535cbc27ec4a871cc1f8 (patch) | |
| tree | 0d72ca2dea9e22e26554c71796987ef74405916f /kernel/type_errors.mli | |
| parent | 0f7e73691dc043f17cf404f9ebbd4185e614e7d3 (diff) | |
Fix dynamic computation of recargs for mutual inductives.
Used by the new guard criterion compatible with type isomorphisms.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions