diff options
| author | Hugo Herbelin | 2020-05-14 21:34:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-14 21:34:17 +0200 |
| commit | 56e23844e80e6d607ad5fa56dfeedcd70e97ee70 (patch) | |
| tree | 403c7b43e73fa4159fd997ca26953098b34e22b5 /test-suite/success | |
| parent | cc54af3842cbf99f169f7937b0e31f737652bd3a (diff) | |
| parent | b5ecd2e46202f47cfccf305e449bcdd8a6a14a0f (diff) | |
Merge PR #12256: Move the static check of evaluability in unfold tactic to runtime.
Reviewed-by: herbelin
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. |