diff options
| author | Matthieu Sozeau | 2014-09-27 16:34:24 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-27 20:41:04 +0200 |
| commit | 0f17c70288662bf8abd1bae59d32a94054481f26 (patch) | |
| tree | f604cd6de5f1274b3e54dcfe48bc84cf0494d473 /dev | |
| parent | 84544396cbbf34848be2240acf181b4d5f1f42d2 (diff) | |
Make pattern_of_constr typed so that we can infer the proper patterns
for primitive projections, fixing bug #3661. Also fix expand_projection
so that it does enough reduction to find the inductive type of its
argument.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions