diff options
| author | Matthieu Sozeau | 2014-09-19 21:10:33 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-19 21:11:13 +0200 |
| commit | 9c2bbdd58b6935ea980e72289777a20b85fe4fdb (patch) | |
| tree | 0ba48b2b60ac76a3d3083001f327f077929202e8 /pretyping/patternops.ml | |
| parent | 2420cdec7290d070de3c7fcfb51caea2cc684d53 (diff) | |
Fixes in Ltac pattern-matching on primitive projections
and pretyping which was not contracting the eta-expanded forms in presence
of coercions.
Diffstat (limited to 'pretyping/patternops.ml')
0 files changed, 0 insertions, 0 deletions