New bugs revealed fixed: #3408 by (probably) Maxime's commits

on vm and #3068 by Nov 2 commit on destruct.

Also fixed test for failure of #3459.

3 files changed, 4 insertions, 4 deletions

diff --git a/test-suite/bugs/opened/3068.v b/test-suite/bugs/closed/3068.v
index 5d3bc0cbc6..7cdd4ea17e 100644
--- a/test-suite/bugs/opened/3068.v
+++ b/test-suite/bugs/closed/3068.v
@@ -57,4 +57,4 @@ Section Finite_nat_set.
     intros H.
     eapply counted_list_equal_nth_char.
     intros i.
-    Fail destruct (counted_def_nth fs1 i _ ) eqn:H0.
+    destruct (counted_def_nth fs1 i _ ) eqn:H0.
diff --git a/test-suite/bugs/opened/3408.v b/test-suite/bugs/closed/3408.v
index 921f641558..b12b8c1afb 100644
--- a/test-suite/bugs/opened/3408.v
+++ b/test-suite/bugs/closed/3408.v
@@ -160,4 +160,4 @@ eapply acc_Abs.
 Defined.
 
 Time Eval native_compute in sizeF_delay (build_large 2).
-Fail Time Eval native_compute in sizeF_guard (build_large 2).
+Time Eval native_compute in sizeF_guard (build_large 2).
diff --git a/test-suite/bugs/opened/3459.v b/test-suite/bugs/opened/3459.v
index 949cace1dc..7c01330990 100644
--- a/test-suite/bugs/opened/3459.v
+++ b/test-suite/bugs/opened/3459.v
@@ -12,8 +12,8 @@ match goal with
                                                        exact r)$) in
                            pose y
 end.
-(* Add extra test for typability *)
-match goal with P:?c |- _ => try (let x := type of c in idtac) || fail 2 end.
+(* Add extra test for typability (should not fail when bug closed) *)
+Fail match goal with P:?c |- _ => try (let x := type of c in idtac) || fail 2 end.
 Abort.
 
 (* Second report raising a Not_found at the time of 21 Oct 2014 *)