Data structure telling implicits of local variables is a map in the

intern_env

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

2 files changed, 8 insertions, 8 deletions

diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index b90937a40..97ae56e16 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -53,10 +53,10 @@ fix rectS_fix n (p: t (S n)): P n p:=
   end.
 
 Definition rect2 (P: forall {n} (a b: t n), Type)
-  (H0: forall n, P (S n) F1 F1)
-  (H1: forall n (f: t n), P (S n) F1 (FS f))
-  (H2: forall n (f: t n), P (S n) (FS f) F1)
-  (HS: forall n (f g : t n), P n f g -> P (S n) (FS f) (FS g)):
+  (H0: forall n, P F1 F1)
+  (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 :=
 match a with
@@ -64,7 +64,7 @@ match a with
                    return match n' as n0
                           return t n0 -> Type with
                             |0 => fun _ => @ID
-                            |S n0 => fun b0 => P (S n0) 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 (S n0) (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 e5bb66a20..150342ee8 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -34,8 +34,8 @@ Section SCHEMES.
 
 (** An induction scheme for non-empty vectors *)
 Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
- (bas: forall a: A, P 0 (a :: []))
- (rect: forall a {n} (v: t A (S n)), P n v -> P (S n) (a :: v)) :=
+ (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 :=
  match v with
  |nil => @id