diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-10-22 15:16:33 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-10-22 15:17:24 +0200 |
| commit | cb93c558cc3d30a486d45f4e4c54799e1a9c889f (patch) | |
| tree | d2c1c199ae8dfce3f7b1acc080f87274af6c7ac5 /test-suite | |
| parent | 21a9cec02cc389a33cf1fc0dc6d0229939abc51d (diff) | |
Fix test-suite for #2729.
Was always failing due to an incorrect use of Ltac's or.
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 *) |