diff options
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. |