Vectors fully use implicit arguments

and take disavantages for maximal insertion

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

1 files changed, 11 insertions, 11 deletions

diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index 1fa70a60c..a576315e6 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -23,7 +23,7 @@ Lemma eq_nth_iff A n (v1 v2: t A n):
   (forall p1 p2, p1 = p2 -> v1 [@ p1 ] = v2 [@ p2 ]) <-> v1 = v2.
 Proof.
 split.
-  revert n v1 v2; refine (rect2 _ _ _); simpl; intros.
+  revert n v1 v2; refine (@rect2 _ _ _ _ _); simpl; intros.
     reflexivity.
     f_equal. apply (H0 Fin.F1 Fin.F1 eq_refl).
     apply H. intros p1 p2 H1;
@@ -34,7 +34,7 @@ Qed.
 Lemma nth_order_last A: forall n (v: t A (S n)) (H: n < S n),
  nth_order v H = last v.
 Proof.
-unfold nth_order; refine (rectS _ _ _); now simpl.
+unfold nth_order; refine (@rectS _ _ _ _); now simpl.
 Qed.
 
 Lemma shiftin_nth A a n (v: t A n) k1 k2 (eq: k1 = k2):
@@ -42,7 +42,7 @@ Lemma shiftin_nth A a n (v: t A n) k1 k2 (eq: k1 = k2):
 Proof.
 subst k2; induction k1.
   generalize dependent n. apply caseS ; intros. now simpl.
-  generalize dependent n. refine (caseS _ _) ; intros. now simpl.
+  generalize dependent n. refine (@caseS _ _ _) ; intros. now simpl.
 Qed.
 
 Lemma shiftin_last A a n (v: t A n): last (shiftin a v) = a.
@@ -53,8 +53,8 @@ Qed.
 Lemma shiftrepeat_nth A: forall n k (v: t A (S n)),
   nth (shiftrepeat v) (Fin.L_R 1 k) = nth v k.
 Proof.
-refine (Fin.rectS _ _ _); intros.
-  revert n v; refine (caseS _ _); simpl; intros. now destruct t.
+refine (@Fin.rectS _ _ _); intros.
+  revert n v; refine (@caseS _ _ _); simpl; intros. now destruct t.
   revert p H.
   refine (match v as v' in t _ m return match m as m' return t A m' -> Type with
     |S (S n) => fun v => forall p : Fin.t (S n),
@@ -66,7 +66,7 @@ Qed.
 
 Lemma shiftrepeat_last A: forall n (v: t A (S n)), last (shiftrepeat v) = last v.
 Proof.
-refine (rectS _ _ _); now simpl.
+refine (@rectS _ _ _ _); now simpl.
 Qed.
 
 Lemma const_nth A (a: A) n (p: Fin.t n): (const a n)[@ p] = a.
@@ -78,17 +78,17 @@ Lemma nth_map {A B} (f: A -> B) {n} v (p1 p2: Fin.t n) (eq: p1 = p2):
   (map f v) [@ p1] = f (v [@ p2]).
 Proof.
 subst p2; induction p1.
-  revert n v; refine (caseS _ _); now simpl.
-  revert n v p1 IHp1; refine (caseS _ _); now simpl.
+  revert n v; refine (@caseS _ _ _); now simpl.
+  revert n v p1 IHp1; refine (@caseS _  _ _); now simpl.
 Qed.
 
 Lemma nth_map2 {A B C} (f: A -> B -> C) {n} v w (p1 p2 p3: Fin.t n):
   p1 = p2 -> p2 = p3 -> (map2 f v w) [@p1] = f (v[@p2]) (w[@p3]).
 Proof.
 intros; subst p2; subst p3; revert n v w p1.
-refine (rect2 _ _ _); simpl.
-  exact (Fin.case0).
-  intros n v1 v2 H a b p; revert n p v1 v2 H; refine (Fin.caseS _ _ _);
+refine (@rect2 _ _ _ _ _); simpl.
+  exact (Fin.case0 _).
+  intros n v1 v2 H a b p; revert n p v1 v2 H; refine (@Fin.caseS _ _ _);
     now simpl.
 Qed.