diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/2729.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/2729.v b/test-suite/bugs/closed/2729.v index c0a4adcb3..7929b8810 100644 --- a/test-suite/bugs/closed/2729.v +++ b/test-suite/bugs/closed/2729.v @@ -11,7 +11,7 @@ Goal forall d:A, match d with C a b => b end = match d with C a b => b end. intro. vm_compute. (* Now check that it is well-typed *) -match goal with |- ?c = _ => try (let x := type of c in idtac) || fail 2 end. +match goal with |- ?c = _ => first [let x := type of c in idtac | fail 2] end. Abort. (* A simplified form of the second problem *) @@ -31,7 +31,7 @@ Lemma L : Proof. vm_compute. (* Now check that it is well-typed (the "P w" used to be turned into "P s") *) -match goal with |- ?c => try (let x := type of c in idtac) || fail 2 end. +match goal with |- ?c => first [let x := type of c in idtac | fail 2] end. Abort. (* Then the original report *) |