diff options
| author | Pierre-Marie Pédrot | 2020-05-05 14:19:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-14 12:38:08 +0200 |
| commit | be56f39ecfc0726772cc6930dbc7657348f008e1 (patch) | |
| tree | f8405fd9fbfb209a037d979b60efeb44dd928438 /test-suite/success | |
| parent | 6f2b88649ec0c1e27befe7bcd2cdbec0ccee95d6 (diff) | |
Move the static check of evaluability in unfold tactic to runtime.
See #11840 for a motivation. I had to fix Floats.FloatLemmas because
it uses the same name for a notation and a term, and the fact this
unfold was working on this was clearly a bug. I hope nobody relies
on this kind of stuff in the wild.
Fixes #5764: "Cannot coerce ..." should be a runtime error.
Fixes #5159: "Cannot coerce ..." should not be an error.
Fixes #4925: unfold gives error on Admitted.
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/with_strategy.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v index 077b57c87f..6f0833211e 100644 --- a/test-suite/success/with_strategy.v +++ b/test-suite/success/with_strategy.v @@ -195,8 +195,8 @@ Opaque F.id. Goal F.id 0 = F.id 0. Fail unfold F.id. - (* This should work, but it fails with "Cannot coerce F.id to an evaluable reference." *) - Fail F.with_transparent_id ltac:(progress unfold F.id). + F.with_transparent_id ltac:(progress unfold F.id). + Undo. F.with_transparent_id ltac:(let x := constr:(@F.id) in progress unfold x). Abort. @@ -212,8 +212,8 @@ Opaque F2.id. Goal F2.id 0 = F2.id 0. Fail unfold F2.id. - (* This should work, but it fails with "Cannot coerce F2.id to an evaluable reference." *) - Fail F2.with_transparent_id ltac:(progress unfold F2.id). + F2.with_transparent_id ltac:(progress unfold F2.id). + Undo. F2.with_transparent_id ltac:(let x := constr:(@F2.id) in progress unfold x). Abort. |