Interp a definition with the implicit arguments of its local context

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

2 files changed, 14 insertions, 14 deletions

diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index 97ae56e16..19b4c3b2f 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -57,14 +57,14 @@ Definition rect2 (P: forall {n} (a b: t n), Type)
   (H1: forall n (f: t n), P F1 (FS f))
   (H2: forall n (f: t n), P (FS f) F1)
   (HS: forall n (f g : t n), P f g -> P (FS f) (FS g)):
-    forall n (a b: t n), P n a b :=
-fix rect2_fix n (a: t n): forall (b: t n), P n a b :=
+    forall n (a b: t n), P a b :=
+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
+                            |S n0 => fun b0 => P F1 b0
                           end b' with
                      |F1 m' => H0 m'
                      |FS m' b' => H1 m' b'
@@ -74,7 +74,7 @@ match a with
                              return t n0 -> Type with
                                |0 => fun _ => @ID
                                |S n0 => fun b0 =>
-                                 forall (a0: t n0), P _ (FS a0) b0
+                                 forall (a0: t n0), P (FS a0) b0
                              end b' with
                          |F1 m' => fun aa => H2 m' aa
                          |FS m' b' => fun aa => HS m' aa b' (rect2_fix m' aa b')
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 0fb6e7acb..807748edd 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -36,21 +36,21 @@ Section SCHEMES.
 Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
  (bas: forall a: A, P (a :: []))
  (rect: forall a {n} (v: t A (S n)), P v -> P (a :: v)) :=
- fix rectS_fix {n} (v: t A (S n)) : P n v :=
+ fix rectS_fix {n} (v: t A (S n)) : P v :=
  match v with
  |nil => @id
  |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 0 (a :: vm)
+         |0 => fun vm => P (a :: vm)
          |S _ => fun _ => ID
          end vnn
      with
      |nil => bas a
      |_ :: _ => @id
      end
- |cons a (S nn') v => rect a _ v (rectS_fix v)
+ |cons a (S nn') v => rect a v (rectS_fix v)
  end.
 
 (** An induction scheme for 2 vectors of same length *)
@@ -104,7 +104,7 @@ Definition hd {A} {n} (v:t A (S n)) := Eval cbv delta beta in
 
 (** The last element of an non empty vector *)
 Definition last {A} {n} (v : t A (S n)) := Eval cbv delta in
-(rectS (fun _ _ => A) (fun a => a) (fun _ _ _ H => H) _ v).
+(rectS (fun _ _ => A) (fun a => a) (fun _ _ _ H => H) v).
 
 (** Build a vector of n{^ th} [a] *)
 Fixpoint const {A} (a:A) (n:nat) :=
@@ -147,7 +147,7 @@ Definition tl {A} {n} (v:t A (S n)) := Eval cbv delta beta in
 (** Remove last element of a non-empty vector *)
 Definition shiftout {A} {n:nat} (v:t A (S n)) : t A n :=
 Eval cbv delta beta in (rectS (fun n _ => t A n) (fun a => [])
-  (fun h _ _ H => h :: H) _ v).
+  (fun h _ _ H => h :: H) v).
 
 (** Add an element at the end of a vector *)
 Fixpoint shiftin {A} {n:nat} (a : A) (v:t A n) : t A (S n) :=
@@ -159,7 +159,7 @@ end.
 (** Copy last element of a vector *)
 Definition shiftrepeat {A} {n} (v:t A (S n)) : t A (S (S n)) :=
 Eval cbv delta beta in (rectS (fun n _ => t A (S (S n)))
-  (fun h =>  h :: h :: []) (fun h _ _ H => h :: H) _ v).
+  (fun h =>  h :: h :: []) (fun h _ _ H => h :: H) v).
 
 (** Remove [p] last elements of a vector *)
 Lemma trunc : forall {A} {n} (p:nat), n > p -> t A n
@@ -229,13 +229,13 @@ Definition map {A} {B} (f : A -> B) : forall {n} (v:t A n), t B n :=
 Definition map2 {A B C}{n} (g:A -> B -> C) (v1:t A n) (v2:t B n)
   : t C n :=
 Eval cbv delta beta in rect2 (fun n _ _ => t C n) (nil C)
-  (fun _ _ _ H a b => (g a b) :: H) _ v1 v2.
+  (fun _ _ _ H a b => (g a b) :: H) v1 v2.
 
 (** fold_left f b [x1 .. xn] = f .. (f (f b x1) x2) .. xn *)
 Definition fold_left {A B:Type} (f:B->A->B): forall (b:B) {n} (v:t A n), B :=
-  fix fold_left_fix (b:B) n (v : t A n) : B := match v with
+  fix fold_left_fix (b:B) {n} (v : t A n) : B := match v with
     | [] => b
-    | a :: w => (fold_left_fix (f b a) _ w)
+    | a :: w => (fold_left_fix (f b a) w)
   end.
 
 (** fold_right f [x1 .. xn] b = f x1 (f x2 .. (f xn b) .. ) *)
@@ -251,7 +251,7 @@ Definition fold_right {A B : Type} (f : A->B->B) :=
 Definition fold_right2 {A B C} (g:A -> B -> C -> C) {n} (v:t A n)
   (w : t B n) (c:C) : C :=
 Eval cbv delta beta in rect2 (fun _ _ _ => C) c
-  (fun _ _ _ H a b => g a b H) _ v w.
+  (fun _ _ _ H a b => g a b H) v w.
 
 (** fold_left2 f b [x1 .. xn] [y1 .. yn] = g .. (g (g a x1 y1) x2 y2) .. xn yn *)
 Definition fold_left2 {A B C: Type} (f : A -> B -> C -> A) :=