diff options
| author | Hugo Herbelin | 2014-10-26 14:23:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-26 15:26:22 +0100 |
| commit | 29a5127dac6d4fbc317e38452cf0fe05916adc56 (patch) | |
| tree | adabfae9b7e860ef3e6aacb4b9f9f3871c6a71dc /kernel/type_errors.mli | |
| parent | 1be28ac589a6affa81b905bbf223bdf520511a44 (diff) | |
Fixing destruct/induction with a using clause on a non-inductive type,
that was broken by commit bf01856940 + use types from induction scheme
to restrict selection of pattern + accept matching from partially
applied term when using "using".
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions