diff options
| author | Hugo Herbelin | 2014-12-09 17:28:37 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-10 15:37:00 +0100 |
| commit | 3e935b3af6ab35ed0bda93087cd784ea1427b536 (patch) | |
| tree | 3fd6ddfb4af9b09a0665b5dea127c4afdf9f9786 /kernel/reduction.ml | |
| parent | b8f0f414f16371299ea93c6f84d5e41886bcf9e4 (diff) | |
Using a more aggressive test for resolving pattern equations ?n = ?p:
test pattern-unification after restriction of the evars so as to
succeed earlier (no observational changes however in the examples at my
disposal).
Diffstat (limited to 'kernel/reduction.ml')
0 files changed, 0 insertions, 0 deletions