Vectors use a bit more the pattern matching compiler

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14773 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 13 insertions, 25 deletions

diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index d6ffef6c4..28e355fb6 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -55,23 +55,16 @@ Definition rect2 (P: forall {n} (a b: t n), Type)
 fix rect2_fix {n} (a: t n): forall (b: t n), P a b :=
 match a with
   |F1 m => fun (b: t (S m)) => match b as b' in t n'
-                   return match n' as n0
-                          return t n0 -> Type with
-                            |0 => fun _ => @ID
-                            |S n0 => fun b0 => P F1 b0
-                          end b' with
+                   return match n',b' with
+                            |0,_ => @ID
+                            |S n0,b0 => P F1 b0
+                          end with
                      |F1 m' => H0 m'
                      |FS m' b' => H1 b'
                    end
-  |FS m a' => fun (b: t (S m)) => match b as b' in t n'
-                      return match n' as n0
-                             return t n0 -> Type with
-                               |0 => fun _ => @ID
-                               |S n0 => fun b0 =>
-                                 forall (a0: t n0), P (FS a0) b0
-                             end b' with
-                         |F1 m' => fun aa => H2 aa
-                         |FS m' b' => fun aa => HS aa b' (rect2_fix aa b')
+  |FS m a' => fun (b: t (S m)) => match b with
+                         |F1 m' => fun aa: t m' => H2 aa
+                         |FS m' b' => fun aa: t m' => HS aa b' (rect2_fix aa b')
                        end a'
 end.
 End SCHEMES.
@@ -123,8 +116,7 @@ Fixpoint weak {m}{n} p (f : t m -> t n) :
   t (p + m) -> t (p + n) :=
 match p as p' return t (p' + m) -> t (p' + n) with
   |0 => f
-  |S p' => fun x => match x in t n0 return
-     match n0 with |0 => @ID |S n0' => n0' = p' + m -> t (S p' + n) end with
+  |S p' => fun x => match x with
      |F1 n' => fun eq : n' = p' + m => F1
      |FS n' y => fun eq : n' = p' + m => FS (weak p' f (eq_rect _ t y _ eq))
   end (eq_refl _)
@@ -149,8 +141,8 @@ Definition L_R {m} n (p : t m) : t (n + m).
 induction n.
   exact p.
   exact ((fix LS k (p: t k) :=
-    match p in t n0 return t (S n0) with
-      |F1 _ => F1
+    match p with
+      |F1 k' => @F1 (S k')
       |FS _ p' => FS (LS _ p')
     end) _ IHn).
 Defined.
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index b4aefbcb1..0fee50ffb 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -69,11 +69,7 @@ match v1 as v1' in t _ n1
        |_ :: _ => @id
      end
   |h1 :: t1 => fun v2 =>
-    match v2 as v2' in t _ n2
-      return match n2, v2' with
-        |0, _ => ID
-        |S n', v2 => forall t1' : t A n', P (h1 :: t1') v2
-        end with
+    match v2 with
       |[] => @id
       |h2 :: t2 => fun t1' =>
         rect (rect2_fix t1' t2) h1 h2
@@ -128,9 +124,9 @@ Definition nth_order {A} {n} (v: t A n) {p} (H: p < n) :=
 
 (** Put [a] at the p{^ th} place of [v] *)
 Fixpoint replace {A n} (v : t A n) (p: Fin.t n) (a : A) {struct p}: t A n :=
-  match p in Fin.t j return t A j -> t A j with
+  match p with
   |Fin.F1 k => fun v': t A (S k) => caseS (fun n _ => t A (S n)) (fun h _ t => a :: t) v'
-  |Fin.FS k p' => fun v': t A (S k) =>
+  |Fin.FS k p' => fun v' =>
     (caseS (fun n _ => Fin.t n -> t A (S n)) (fun h _ t p2 => h :: (replace t p2 a)) v') p'
   end v.