From cb93c558cc3d30a486d45f4e4c54799e1a9c889f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 22 Oct 2014 15:16:33 +0200 Subject: Fix test-suite for #2729. Was always failing due to an incorrect use of Ltac's or. --- test-suite/bugs/closed/2729.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'test-suite') 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 *) -- cgit v1.2.3