From 158398435d1727e59f933f3eff6b58c5a635ffb8 Mon Sep 17 00:00:00 2001
From: Xavier Clerc <xavier.clerc@inria.fr>
Date: Fri, 26 Sep 2014 13:29:36 +0200
Subject: Add missing "Fail" to bug cases.

---
 test-suite/bugs/opened/3509.v | 2 +-
 test-suite/bugs/opened/3510.v | 2 +-
 test-suite/bugs/opened/3554.v | 2 +-
 test-suite/bugs/opened/3562.v | 2 +-
 test-suite/bugs/opened/3618.v | 2 +-
 test-suite/bugs/opened/3625.v | 6 +++---
 test-suite/bugs/opened/3626.v | 6 +++---
 test-suite/bugs/opened/3628.v | 2 +-
 test-suite/bugs/opened/3655.v | 2 +-
 test-suite/bugs/opened/3660.v | 2 +-
 10 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/test-suite/bugs/opened/3509.v b/test-suite/bugs/opened/3509.v
index 4c9ba95ab..02e47a8b4 100644
--- a/test-suite/bugs/opened/3509.v
+++ b/test-suite/bugs/opened/3509.v
@@ -15,4 +15,4 @@ Lemma match_bool_comm_1 (b : bool) A B (F : forall x : A, B x) t f
 admit.
 Defined.
 Hint Rewrite match_bool_fn : matchdb.
-Hint Rewrite match_bool_comm_1 : matchdb.
+Fail Hint Rewrite match_bool_comm_1 : matchdb.
diff --git a/test-suite/bugs/opened/3510.v b/test-suite/bugs/opened/3510.v
index 9e5489339..25285636b 100644
--- a/test-suite/bugs/opened/3510.v
+++ b/test-suite/bugs/opened/3510.v
@@ -31,4 +31,4 @@ Lemma match_option_comm_2 T (p : option T) A B R (f : forall (x : A) (y : B x),
       end.
 admit.
 Defined.
-Hint Rewrite match_option_fn match_option_comm_2 : matchdb.
+Fail Hint Rewrite match_option_fn match_option_comm_2 : matchdb.
diff --git a/test-suite/bugs/opened/3554.v b/test-suite/bugs/opened/3554.v
index 13a79cc84..422c5770e 100644
--- a/test-suite/bugs/opened/3554.v
+++ b/test-suite/bugs/opened/3554.v
@@ -1 +1 @@
-Example foo (f : forall {_ : Type}, Type) : Type.
+Fail Example foo (f : forall {_ : Type}, Type) : Type.
diff --git a/test-suite/bugs/opened/3562.v b/test-suite/bugs/opened/3562.v
index cfbdd5554..04a1223b6 100644
--- a/test-suite/bugs/opened/3562.v
+++ b/test-suite/bugs/opened/3562.v
@@ -1,2 +1,2 @@
 Theorem t: True.
-destruct 0 as x.
+Fail destruct 0 as x.
diff --git a/test-suite/bugs/opened/3618.v b/test-suite/bugs/opened/3618.v
index cebfcc20e..bd24c7a7d 100644
--- a/test-suite/bugs/opened/3618.v
+++ b/test-suite/bugs/opened/3618.v
@@ -93,7 +93,7 @@ Class inO {fs : Funext} {subU : ReflectiveSubuniverse} (T : Type) :=
 Global Instance hprop_inO {fs : Funext} {subU : ReflectiveSubuniverse} (T : Type) : IsTrunc (trunc_S minus_two) (inO T) .
 Admitted.
 
-Definition equiv_O_rectnd {fs : Funext} {subU : ReflectiveSubuniverse}
+Fail Definition equiv_O_rectnd {fs : Funext} {subU : ReflectiveSubuniverse}
            (P Q : Type) {Q_inO : inO_internal Q}
 : IsEquiv (fun f => compose f (O_unit P))
 := _.
diff --git a/test-suite/bugs/opened/3625.v b/test-suite/bugs/opened/3625.v
index 02110919b..46a6c009e 100644
--- a/test-suite/bugs/opened/3625.v
+++ b/test-suite/bugs/opened/3625.v
@@ -2,6 +2,6 @@ Set Implicit Arguments.
 Set Primitive Projections.
 Record prod A B := pair { fst : A ; snd : B }.
 
-Goal forall x y : prod Set Set, x.(@fst) = y.(@fst).
-  intros.
-  apply f_equal.
+Fail Goal forall x y : prod Set Set, x.(@fst) = y.(@fst).
+(*  intros.
+    apply f_equal. *)
diff --git a/test-suite/bugs/opened/3626.v b/test-suite/bugs/opened/3626.v
index 02110919b..46a6c009e 100644
--- a/test-suite/bugs/opened/3626.v
+++ b/test-suite/bugs/opened/3626.v
@@ -2,6 +2,6 @@ Set Implicit Arguments.
 Set Primitive Projections.
 Record prod A B := pair { fst : A ; snd : B }.
 
-Goal forall x y : prod Set Set, x.(@fst) = y.(@fst).
-  intros.
-  apply f_equal.
+Fail Goal forall x y : prod Set Set, x.(@fst) = y.(@fst).
+(*  intros.
+    apply f_equal. *)
diff --git a/test-suite/bugs/opened/3628.v b/test-suite/bugs/opened/3628.v
index 4001cf7c2..bd85bb1f9 100644
--- a/test-suite/bugs/opened/3628.v
+++ b/test-suite/bugs/opened/3628.v
@@ -5,5 +5,5 @@ End NonPrim.
 Module Prim.
   Set Primitive Projections.
   Class AClass := { x : Set }.
-  Arguments x {AClass}.
+  Fail Arguments x {AClass}.
 End Prim.
diff --git a/test-suite/bugs/opened/3655.v b/test-suite/bugs/opened/3655.v
index 3ef112b7c..2ec1da64d 100644
--- a/test-suite/bugs/opened/3655.v
+++ b/test-suite/bugs/opened/3655.v
@@ -2,4 +2,4 @@ Ltac bar x := pose x.
 Tactic Notation "foo" open_constr(x) := bar x.
 Class baz := { baz' : Type }.
 Goal True.
-  foo baz'.
+  Fail foo baz'.
diff --git a/test-suite/bugs/opened/3660.v b/test-suite/bugs/opened/3660.v
index 0ee56b5ae..f962e1f04 100644
--- a/test-suite/bugs/opened/3660.v
+++ b/test-suite/bugs/opened/3660.v
@@ -24,4 +24,4 @@ Goal forall (C D : hSet), IsEquiv (fun x : C = D => (equiv_path C D (ap setT x))
   apply @isequiv_compose; [ | admit ].
   solve [ apply isequiv_ap_setT ].
   Undo.
-  typeclasses eauto.
+  Fail typeclasses eauto.
-- 
cgit v1.2.3