From 4598007c8b8bfc7e591e53116e37f49743317fec Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 21 Nov 2011 11:41:20 +0000
Subject: 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
---
 theories/Vectors/Fin.v       | 12 +++---------
 theories/Vectors/VectorDef.v | 18 ++++++++----------
 2 files changed, 11 insertions(+), 19 deletions(-)

(limited to 'theories/Vectors')

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
-- 
cgit v1.2.3