diff options
| author | Pierre-Marie Pédrot | 2020-09-02 21:11:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-04 14:04:48 +0200 |
| commit | f9b5e98e7bc94f0385d1a9a62f3c3d5b9227197f (patch) | |
| tree | 85f605fbc5c6828b7daef125364e48ede43c2460 /dev/include | |
| parent | 950da3527f0383aba8faf79b99a11313e0e9a3fa (diff) | |
Restrict a spurious call to a reduction to a quantified inductive type.
Actually the callers of that function only apply it to an applied
inductive type.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions