diff options
| author | Pierre-Marie Pédrot | 2020-11-21 15:51:30 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-30 18:45:40 +0100 |
| commit | b2d3d5f5d5f3e16e271a124f9f60a09788e93838 (patch) | |
| tree | 6156e3a8846168a40a94b21383d612958f6b526c /dev | |
| parent | 0af89e4c04b1ecf437a86b50a34a17eddee56b76 (diff) | |
Store Ltac2 valexpr instead of unevaluated code inside Ltac1 value embedding.
This should have the same semantics, it is just a matter of moving the
responsibility of evaluating the thunk from the Ltac1 application tactic to
the quotation.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions