Fix test-suite file to test original bug, not the failure of the guard

condition.

1 files changed, 12 insertions, 7 deletions

diff --git a/test-suite/bugs/closed/3350.v b/test-suite/bugs/closed/3350.v
index bab197ed0..30fdf1694 100644
--- a/test-suite/bugs/closed/3350.v
+++ b/test-suite/bugs/closed/3350.v
@@ -9,6 +9,8 @@ Arguments Fin.F1 : clear implicits.
 Lemma fin_0_absurd : notT (Fin.t 0).
 Proof. hnf. apply Fin.case0. Qed.
 
+Axiom admit : forall {A}, A.
+
 Fixpoint lower {n:nat} (p:Fin.t (S n)) {struct p} :
   forall (i:Fin.t (S n)), option (Fin.t n)
   := match p in Fin.t (S n1)
@@ -32,7 +34,7 @@ Fixpoint lower {n:nat} (p:Fin.t (S n)) {struct p} :
                match n2 as n3 return Fin.t n3 -> Fin.t n3 -> option (Fin.t n3) with
                  | 0 => fun i3 p3 => False_rect _ (fin_0_absurd p3)
                  | S n3 => fun (i3 p3:Fin.t (S n3)) =>
-                             option_map (@Fin.FS _) (lower p3 i3)
+                             option_map (@Fin.FS _) admit
                end i2
            end p1
      end.
@@ -66,10 +68,10 @@ Proof.
     clear n1 i1;
     (intros [|n] i; [refine (False_rect _ (fin_0_absurd i)) | cbn ]).
     { apply cS1. }
-    { intros p. pose proof (lower_ind n p i) as H.
+    { intros p. pose proof (admit : P n p i (lower p i)) as H.
       destruct (lower p i) eqn:E.
-      { apply cSSS; assumption. }
-      { cbn. apply cSSN; assumption. } } }
+      { admit; assumption. }
+      { cbn. apply admit; assumption. } } }
 Qed.
 
 Section squeeze.
@@ -92,12 +94,13 @@ Section squeeze.
                 with
                   | Vector.nil _ => tt
                   | Vector.cons _ h _ u' =>
-                    fun j' => Vector.cons _ h _ (squeeze u' j')
+                    fun j' => Vector.cons _ h _ admit (* (squeeze u' j') *)
                 end
           end v' i'
     end v.
 End squeeze.
 
+Require Import Program.
 Lemma squeeze_nth (A:Type) (x:A) (n:nat) (v:Vector.t A n) p i :
   Vector.nth (squeeze x v p) i = match lower p i with
                                    | Some j => Vector.nth v j
@@ -111,5 +114,7 @@ Proof.
 
   (*** Fails here with "Conversion test raised an anomaly" ***)
   revert v.
-
-Abort.
+  admit.
+  admit.
+  admit.
+Qed.