VectorDef.v takes benefit of dependencies being taken into account

between initial terms to match in pattern-matching compilation
algorithm.

Also simplified Fin.v though the simplification was possible
beforehand.

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

2 files changed, 11 insertions, 19 deletions

diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index 980a5f706..d6ffef6c4 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -31,10 +31,7 @@ Definition case0 P (p: t 0): P p :=
 Definition caseS (P: forall {n}, t (S n) -> Type)
   (P1: forall n, @P n F1) (PS : forall {n} (p: t n), P (FS p))
   {n} (p: t (S n)): P p :=
-  match p as p0 in t n0
-  return match n0 as nn return t nn -> Type with
-    |0 => fun _ => @ID |S n' => fun p' => P p'
-  end p0 with
+  match p with
   |F1 k => P1 k
   |FS k pp => PS pp
   end.
@@ -43,10 +40,7 @@ Definition rectS (P: forall {n}, t (S n) -> Type)
   (P1: forall n, @P n F1) (PS : forall {n} (p: t (S n)), P p -> P (FS p)):
   forall {n} (p: t (S n)), P p :=
 fix rectS_fix {n} (p: t (S n)): P p:=
-  match p as p0 in t n0
-  return match n0 as nn return t nn -> Type with
-    |0 => fun _ => @ID |S n' => fun p' => P p'
-  end p0 with
+  match p with
   |F1 k => P1 k
   |FS 0 pp => case0 (fun f => P (FS f)) pp
   |FS (S k) pp => PS pp (rectS_fix pp)
@@ -187,4 +181,4 @@ induction o ; simpl.
   rewrite R_sanity. rewrite IHo.
   rewrite Plus.plus_assoc. destruct (to_nat o); simpl; rewrite Mult.mult_succ_r.
     now rewrite (Plus.plus_comm n).
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index ad241462e..b4aefbcb1 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -44,10 +44,10 @@ Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
  |cons a 0 v =>
    match v as vnn in t _ nn
        return
-         match nn as nnn return t A nnn -> Type with
-         |0 => fun vm => P (a :: vm)
-         |S _ => fun _ => ID
-         end vnn
+         match nn,vnn with
+         |0,vm =>  P (a :: vm)
+         |S _,_ => ID
+         end
      with
      |nil => bas a
      |_ :: _ => @id
@@ -70,12 +70,10 @@ match v1 as v1' in t _ n1
      end
   |h1 :: t1 => fun v2 =>
     match v2 as v2' in t _ n2
-      return match n2 as n2'
-        return t B n2' -> Type with
-        |0 => fun _ => @ID
-        |S n' => fun v2 => forall t1' : t A n',
-          P (h1 :: t1') v2
-        end v2' with
+      return match n2, v2' with
+        |0, _ => ID
+        |S n', v2 => forall t1' : t A n', P (h1 :: t1') v2
+        end with
       |[] => @id
       |h2 :: t2 => fun t1' =>
         rect (rect2_fix t1' t2) h1 h2