diff options
| author | Erik Martin-Dorel | 2019-09-09 19:03:30 -0700 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-09-10 11:57:15 -0700 |
| commit | e4c185319f3511a8794a12b099400015508d76ee (patch) | |
| tree | 767fe6a107f83b2385e68597f4c3d8db42c4f47b /kernel/nativelambda.ml | |
| parent | 638dacdba06fb09898d57106f65afa1c88f5805d (diff) | |
feat: Add a rewrite rule (UnderE) to unprotect evars in subgoals
E.g., if one wish to instantiate these evars manually, in another way
than with reflexivity.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions