diff options
| author | Enrico Tassi | 2015-09-10 11:44:11 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-12-03 09:59:45 +0100 |
| commit | 4d0f111956307c5a134db701fe27f01f8ac50e9d (patch) | |
| tree | 83a8175782bdd7c04d614a269878a0f9ab3e51e7 /mathcomp/attic/tutorial.v | |
| parent | 55a5aaa22e9dd92ff1c6aba599b878c384c1a66b (diff) | |
fix: elim/v handles eliminator from Derive Inversion (issue #2)
Also:
- fix elim trying to saturate too much and not raising the expected exn
- fix fill_occ_pattern when occ is {-}, it used to lose the
instantiation obtained by matching the term
Diffstat (limited to 'mathcomp/attic/tutorial.v')
0 files changed, 0 insertions, 0 deletions