diff options
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/Record.v | 1 | ||||
| -rw-r--r-- | test-suite/success/with_strategy.v | 8 |
2 files changed, 5 insertions, 4 deletions
diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v index 18ebcd6384..ce07512a1e 100644 --- a/test-suite/success/Record.v +++ b/test-suite/success/Record.v @@ -3,6 +3,7 @@ Definition CProp := Prop. Record test : CProp := {n : nat ; m : bool ; _ : n <> 0 }. Require Import Program. Require Import List. +Import ListNotations. Record vector {A : Type} {n : nat} := { vec_list : list A ; vec_len : length vec_list = n }. Arguments vector : clear implicits. 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. |