1 files changed, 55 insertions, 49 deletions
diff --git a/test-suite/success/Case9.v b/test-suite/success/Case9.v
index a5d07405..a8534a0b 100644
--- a/test-suite/success/Case9.v
+++ b/test-suite/success/Case9.v
@@ -1,55 +1,61 @@
-Inductive List [A:Set] :Set := 
- Nil:(List A) | Cons:A->(List A)->(List A).
-
-Inductive eqlong : (List nat)-> (List nat)-> Prop :=
- eql_cons : (n,m:nat)(x,y:(List nat)) 
-            (eqlong x y) -> (eqlong (Cons nat n x) (Cons nat m y))
-| eql_nil :  (eqlong (Nil nat) (Nil nat)).
-
-
-Parameter V1 : (eqlong (Nil nat) (Nil nat))\/ ~(eqlong (Nil nat) (Nil nat)).
-Parameter V2 : (a:nat)(x:(List nat))
-      (eqlong (Nil nat) (Cons nat a x))\/ ~(eqlong (Nil nat)(Cons nat a x)).
-Parameter V3 : (a:nat)(x:(List nat))
-      (eqlong  (Cons nat a x)  (Nil nat))\/ ~(eqlong (Cons nat a x) (Nil nat)).
-Parameter V4 : (a:nat)(x:(List nat))(b:nat)(y:(List nat))
-      (eqlong  (Cons nat a x)(Cons nat b y))
-        \/ ~(eqlong (Cons nat a x) (Cons nat b y)).
-
-Parameter nff : (n,m:nat)(x,y:(List nat)) 
-               ~(eqlong x y)-> ~(eqlong (Cons nat n x) (Cons nat m y)).
-Parameter inv_r : (n:nat)(x:(List nat)) ~(eqlong (Nil nat) (Cons nat n x)).
-Parameter inv_l : (n:nat)(x:(List nat)) ~(eqlong (Cons nat n x) (Nil nat)).
-
-Fixpoint eqlongdec [x:(List nat)]: (y:(List nat))(eqlong x y)\/~(eqlong x y) :=
-[y:(List nat)]
- <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases x y of
-      Nil Nil   => (or_introl ? ~(eqlong (Nil nat) (Nil nat))  eql_nil)
-
-   |  Nil ((Cons a x) as L) =>(or_intror (eqlong (Nil nat) L)  ? (inv_r a x))
-
-   |  ((Cons a x) as L) Nil => (or_intror (eqlong L (Nil nat)) ? (inv_l a x))
-
-   | ((Cons a x) as L1) ((Cons b y) as L2) =>  
-      <(eqlong L1 L2) \/~(eqlong L1 L2)>Cases (eqlongdec x y) of
-        (or_introl h) => (or_introl  ? ~(eqlong L1 L2) (eql_cons a b x y h))
-      | (or_intror h) => (or_intror (eqlong L1 L2) ? (nff a b x y h))   
+Inductive List (A : Set) : Set :=
+  | Nil : List A
+  | Cons : A -> List A -> List A.
+
+Inductive eqlong : List nat -> List nat -> Prop :=
+  | eql_cons :
+      forall (n m : nat) (x y : List nat),
+      eqlong x y -> eqlong (Cons nat n x) (Cons nat m y)
+  | eql_nil : eqlong (Nil nat) (Nil nat).
+
+
+Parameter V1 : eqlong (Nil nat) (Nil nat) \/ ~ eqlong (Nil nat) (Nil nat).
+Parameter
+  V2 :
+    forall (a : nat) (x : List nat),
+    eqlong (Nil nat) (Cons nat a x) \/ ~ eqlong (Nil nat) (Cons nat a x).
+Parameter
+  V3 :
+    forall (a : nat) (x : List nat),
+    eqlong (Cons nat a x) (Nil nat) \/ ~ eqlong (Cons nat a x) (Nil nat).
+Parameter
+  V4 :
+    forall (a : nat) (x : List nat) (b : nat) (y : List nat),
+    eqlong (Cons nat a x) (Cons nat b y) \/
+    ~ eqlong (Cons nat a x) (Cons nat b y).
+
+Parameter
+  nff :
+    forall (n m : nat) (x y : List nat),
+    ~ eqlong x y -> ~ eqlong (Cons nat n x) (Cons nat m y).
+Parameter
+  inv_r : forall (n : nat) (x : List nat), ~ eqlong (Nil nat) (Cons nat n x).
+Parameter
+  inv_l : forall (n : nat) (x : List nat), ~ eqlong (Cons nat n x) (Nil nat).
+
+Fixpoint eqlongdec (x y : List nat) {struct x} :
+ eqlong x y \/ ~ eqlong x y :=
+  match x, y return (eqlong x y \/ ~ eqlong x y) with
+  | Nil, Nil => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil
+  | Nil, Cons a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x)
+  | Cons a x as L, Nil => or_intror (eqlong L (Nil nat)) (inv_l a x)
+  | Cons a x as L1, Cons b y as L2 =>
+      match eqlongdec x y return (eqlong L1 L2 \/ ~ eqlong L1 L2) with
+      | or_introl h => or_introl (~ eqlong L1 L2) (eql_cons a b x y h)
+      | or_intror h => or_intror (eqlong L1 L2) (nff a b x y h)
       end
- end.
+  end.
 
 
 Type
- <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases (Nil nat) (Nil nat) of
-      Nil Nil   => (or_introl ? ~(eqlong (Nil nat) (Nil nat))  eql_nil)
-
-   |  Nil ((Cons a x) as L) =>(or_intror (eqlong (Nil nat) L)  ? (inv_r a x))
-
-   |  ((Cons a x) as L) Nil => (or_intror (eqlong L (Nil nat)) ? (inv_l a x))
-
-   | ((Cons a x) as L1) ((Cons b y) as L2) =>  
-      <(eqlong L1 L2) \/~(eqlong L1 L2)>Cases (eqlongdec x y) of
-        (or_introl h) => (or_introl  ? ~(eqlong L1 L2) (eql_cons a b x y h))
-      | (or_intror h) => (or_intror (eqlong L1 L2) ? (nff a b x y h))   
+  match Nil nat as x, Nil nat as y return (eqlong x y \/ ~ eqlong x y) with
+  | Nil, Nil => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil
+  | Nil, Cons a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x)
+  | Cons a x as L, Nil => or_intror (eqlong L (Nil nat)) (inv_l a x)
+  | Cons a x as L1, Cons b y as L2 =>
+      match eqlongdec x y return (eqlong L1 L2 \/ ~ eqlong L1 L2) with
+      | or_introl h => or_introl (~ eqlong L1 L2) (eql_cons a b x y h)
+      | or_intror h => or_intror (eqlong L1 L2) (nff a b x y h)
       end
- end.
+  end.