diff options
| author | Pierre-Marie Pédrot | 2018-08-13 19:47:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-08-13 20:40:23 +0200 |
| commit | 5fcbb0eb7b624ee18b817e7fd1b3b0d2fbc9bd35 (patch) | |
| tree | 7072e91deaa91a9a37385d20f7cfc5d4c49f6cb6 /kernel/nativelambda.ml | |
| parent | 18b662aa306c58d46292bdf79a2929c91d7d96fd (diff) | |
Less crazy implementation of the "pose" family of tactics.
The previous implementation was calling a lot of useless unification
even though the net effect of the tactic was simply to add a binding to
the environment.
Interestingly the base tactic was used in several higher level tactics,
including evar and ssreflect pose.
Part of the fix for #8245.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions