Modify Vectors/VectorSpec.v to compile with -mangle-names

1 files changed, 44 insertions, 44 deletions

diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index 443931e5bb..10545332bb 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -26,7 +26,7 @@ Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n}
 
 Lemma eta {A} {n} (v : t A (S n)) : v = hd v :: tl v.
 Proof.
-intros; apply caseS with (v:=v); intros; reflexivity.
+intros; apply (fun P IS => caseS P IS (n := n) v); intros; reflexivity.
 Defined.
 
 (** Lemmas are done for functions that use [Fin.t] but thanks to [Peano_dec.le_unique], all
@@ -38,9 +38,9 @@ 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.
   + reflexivity.
-  + f_equal. apply (H0 Fin.F1 Fin.F1 eq_refl).
+  + intros n ? ? H ? ? H0. f_equal. apply (H0 Fin.F1 Fin.F1 eq_refl).
     apply H. intros p1 p2 H1;
     apply (H0 (Fin.FS p1) (Fin.FS p2) (f_equal (@Fin.FS n) H1)).
 - intros; now f_equal.
@@ -48,12 +48,12 @@ Qed.
 
 Lemma nth_order_hd A: forall n (v : t A (S n)) (H : 0 < S n),
   nth_order v H = hd v.
-Proof. intros; now rewrite (eta v). Qed.
+Proof. intros n v H; now rewrite (eta v). Qed.
 
 Lemma nth_order_tl A: forall n k (v : t A (S n)) (H : k < n) (HS : S k < S n),
   nth_order (tl v) H = nth_order v HS.
 Proof.
-induction n; intros.
+intros n; induction n; intros k v H HS.
 - inversion H.
 - rewrite (eta v).
   unfold nth_order; simpl.
@@ -69,7 +69,7 @@ Qed.
 Lemma nth_order_ext A: forall n k (v : t A n) (H1 H2 : k < n),
   nth_order v H1 = nth_order v H2.
 Proof.
-intros; unfold nth_order.
+intros n k v H1 H2; unfold nth_order.
 now rewrite (Fin.of_nat_ext H1 H2).
 Qed.
 
@@ -78,7 +78,7 @@ Qed.
 Lemma shiftin_nth A a n (v: t A n) k1 k2 (eq: k1 = k2):
   nth (shiftin a v) (Fin.L_R 1 k1) = nth v k2.
 Proof.
-subst k2; induction k1.
+subst k2; induction k1 as [n|n k1].
 - generalize dependent n. apply caseS ; intros. now simpl.
 - generalize dependent n. refine (@caseS _ _ _) ; intros. now simpl.
 Qed.
@@ -92,14 +92,14 @@ 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 _ _ _); lazy beta; [ intros n v | intros n p H v ].
-- revert n v; refine (@caseS _ _ _); simpl; intros. now destruct t.
+- revert n v; refine (@caseS _ _ _); simpl; intros ? ? t. now destruct t.
 - revert p H.
   refine (match v as v' in t _ m return match m as m' return t A m' -> Prop with
     |S (S n) => fun v => forall p : Fin.t (S n),
       (forall v0 : t A (S n), (shiftrepeat v0) [@ Fin.L_R 1 p ] = v0 [@p]) ->
       (shiftrepeat v) [@Fin.L_R 1 (Fin.FS p)] = v [@Fin.FS p]
     |_ => fun _ => True end v' with
-  |[] => I |h :: t => _ end). destruct n0. exact I. now simpl.
+  |[] => I | cons _ h n t => _ end). destruct n. exact I. now simpl.
 Qed.
 
 Lemma shiftrepeat_last A: forall n (v: t A (S n)), last (shiftrepeat v) = last v.
@@ -112,7 +112,7 @@ Qed.
 Lemma nth_order_replace_eq A: forall n k (v : t A n) a (H1 : k < n) (H2 : k < n),
   nth_order (replace v (Fin.of_nat_lt H2) a) H1 = a.
 Proof.
-intros n k; revert n; induction k; intros;
+intros n k; revert n; induction k as [|k IHk]; intros n v a H1 H2;
   (destruct n; [ inversion H1 | subst ]).
 - now rewrite nth_order_hd, (eta v).
 - rewrite <- (nth_order_tl _ _ _ _ (proj2 (Nat.succ_lt_mono _ _) H1)), (eta v).
@@ -123,7 +123,7 @@ Lemma nth_order_replace_neq A: forall n k1 k2, k1 <> k2 ->
   forall (v : t A n) a (H1 : k1 < n) (H2 : k2 < n),
   nth_order (replace v (Fin.of_nat_lt H2) a) H1 = nth_order v H1.
 Proof.
-intros n k1; revert n; induction k1; intros;
+intros n k1; revert n; induction k1 as [|k1 IHk1]; intros n k2 H v a H1 H2;
   (destruct n ; [ inversion H1 | subst ]).
 - rewrite 2 nth_order_hd.
   destruct k2; intuition.
@@ -137,15 +137,15 @@ Qed.
 Lemma replace_id A: forall n p (v : t A n),
   replace v p (nth v p) = v.
 Proof.
-induction p; intros; rewrite 2 (eta v); simpl; auto.
+intros n p; induction p as [|? p IHp]; intros v; rewrite 2 (eta v); simpl; auto.
 now rewrite IHp.
 Qed.
 
 Lemma replace_replace_eq A: forall n p (v : t A n) a b,
   replace (replace v p a) p b = replace v p b.
 Proof.
-intros.
-induction p; rewrite 2 (eta v); simpl; auto.
+intros n p v a b.
+induction p as [|? p IHp]; rewrite 2 (eta v); simpl; auto.
 now rewrite IHp.
 Qed.
 
@@ -161,7 +161,7 @@ apply (Fin.rect2 (fun n p1 p2 => forall v a b,
 - intros n p1 v; revert n v p1.
   refine (@rectS _ _ _ _); auto.
 - intros n p1 p2 IH v; revert n v p1 p2 IH.
-  refine (@rectS _ _ _ _); simpl; do 6 intro; [ | do 3 intro ]; intro Hneq;
+  refine (@rectS _ _ _ _); simpl; intro n; [| do 3 intro]; intros ? ? IH p1 p2; intro Hneq;
     f_equal; apply IH; intros Heq; apply Hneq; now subst.
 Qed.
 
@@ -177,19 +177,19 @@ Qed.
 Lemma map_id A: forall n (v : t A n),
   map (fun x => x) v = v.
 Proof.
-induction v; simpl; [ | rewrite IHv ]; auto.
+intros n v; induction v as [|? ? v IHv]; simpl; [ | rewrite IHv ]; auto.
 Qed.
 
 Lemma map_map A B C: forall (f:A->B) (g:B->C) n (v : t A n),
   map g (map f v) = map (fun x => g (f x)) v.
 Proof.
-induction v; simpl; [ | rewrite IHv ]; auto.
+intros f g n v; induction v as [|? ? v IHv]; simpl; [ | rewrite IHv ]; auto.
 Qed.
 
 Lemma map_ext_in A B: forall (f g:A->B) n (v : t A n),
   (forall a, In a v -> f a = g a) -> map f v = map g v.
 Proof.
-induction v; simpl; auto.
+intros f g n v H; induction v as [|? ? v IHv]; simpl; auto.
 intros; rewrite H by constructor; rewrite IHv; intuition.
 apply H; now constructor.
 Qed.
@@ -203,7 +203,7 @@ Qed.
 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.
+subst p2; induction p1 as [n|n p1 IHp1].
 - revert n v; refine (@caseS _ _ _); now simpl.
 - revert n v p1 IHp1; refine (@caseS _  _ _); now simpl.
 Qed.
@@ -225,10 +225,10 @@ Lemma fold_left_right_assoc_eq {A B} {f: A -> B -> A}
   {n} (v: t B n): forall a, fold_left f a v = fold_right (fun x y => f y x) v a.
 Proof.
 assert (forall n h (v: t B n) a, fold_left f (f a h) v = f (fold_left f a v) h).
-- induction v0.
+- intros n0 h v0; induction v0 as [|? ? v0 IHv0].
   + now simpl.
   + intros; simpl. rewrite<- IHv0, assoc. now f_equal.
-- induction v.
+- induction v as [|? ? v IHv].
   + reflexivity.
   + simpl. intros; now rewrite<- (IHv).
 Qed.
@@ -245,31 +245,31 @@ Qed.
 (** ** Properties of [take] *)
 
 Lemma take_O : forall {A} {n} le (v:t A n), take 0 le v = [].
-Proof. 
+Proof.
   reflexivity.
-Qed. 
+Qed.
 
 Lemma take_idem : forall {A} p n (v:t A n)  le le', 
   take p le' (take p le v) = take p le v.
-Proof. 
-  induction p; intros n v le le'.
-  - auto. 
-  - destruct v. inversion le. simpl. apply f_equal. apply IHp. 
+Proof.
+  intros A p; induction p as [|p IHp]; intros n v le le'.
+  - auto.
+  - destruct v. inversion le. simpl. apply f_equal. apply IHp.
 Qed.
 
 Lemma take_app : forall {A} {n} (v:t A n) {m} (w:t A m) le, take n le (append v w) = v.
-Proof. 
-  induction v; intros m w le.
-  - reflexivity. 
-  - simpl. apply f_equal. apply IHv. 
+Proof.
+  intros a n v; induction v as [|? ? v IHv]; intros m w le.
+  - reflexivity.
+  - simpl. apply f_equal. apply IHv.
 Qed.
 
 (* Proof is irrelevant for [take] *)
 Lemma take_prf_irr : forall {A} p {n} (v:t A n) le le', take p le v = take p le' v.
-Proof. 
-  induction p; intros n v le le'. 
-  - reflexivity.  
-  - destruct v. inversion le. simpl. apply f_equal. apply IHp. 
+Proof.
+  intros A p; induction p as [|p IHp]; intros n v le le'.
+  - reflexivity.
+  - destruct v. inversion le. simpl. apply f_equal. apply IHp.
 Qed.
 
 (** ** Properties of [uncons] and [splitat] *)
@@ -289,7 +289,7 @@ Lemma splitat_append {A} : forall {n m : nat} (v : t A n) (w : t A m),
 Proof with simpl; auto.
   intros n m v.
   generalize dependent m.
-  induction v; intros...
+  induction v as [|? ? v IHv]; intros...
   rewrite IHv...
 Qed.
 
@@ -299,10 +299,10 @@ Lemma append_splitat {A} : forall {n m : nat} (v : t A n) (w : t A m) (vw : t A
 Proof with auto.
   intros n m v.
   generalize dependent m.
-  induction v; intros; inversion H...
+  induction v as [|a n v IHv]; intros m w vw H; inversion H as [H1]...
   destruct (splitat n (tl vw)) as [v' w'] eqn:Heq.
   apply pair_equal_spec in H1.
-  destruct H1; subst.
+  destruct H1 as [H0]; subst.
   rewrite <- append_comm_cons.
   rewrite (eta vw).
   apply cons_inj in H0.
@@ -316,7 +316,7 @@ Qed.
 Lemma Forall_impl A: forall (P Q : A -> Prop), (forall a, P a -> Q a) ->
   forall n (v : t A n), Forall P v -> Forall Q v.
 Proof.
-induction v; intros HP; constructor; inversion HP as [| ? ? ? ? ? Heq1 [Heq2 He]];
+intros P Q H n v; induction v; intros HP; constructor; inversion HP as [| ? ? ? ? ? Heq1 [Heq2 He]];
   apply (inj_pair2_eq_dec _ Nat.eq_dec) in He; subst; intuition.
 Qed.
 
@@ -328,7 +328,7 @@ intros P n v; split.
   revert HP; induction Hin; intros HP;
     inversion HP as [| ? ? ? ? ? Heq1 [Heq2 He]]; subst; auto.
   apply (inj_pair2_eq_dec _ Nat.eq_dec) in He; subst; auto.
-- induction v; intros Hin; constructor.
+- induction v as [|? ? v IHv]; intros Hin; constructor.
   + apply Hin; constructor.
   + apply IHv; intros a Ha.
     apply Hin; now constructor.
@@ -337,7 +337,7 @@ Qed.
 Lemma Forall_nth_order A: forall P n (v : t A n),
   Forall P v <-> forall i (Hi : i < n), P (nth_order v Hi).
 Proof.
-split; induction n.
+intros P n v; split; induction n as [|n IHn].
 - intros HF i Hi; inversion Hi.
 - intros HF i Hi.
   rewrite (eta v).
@@ -354,7 +354,7 @@ split; induction n.
   rewrite (eta v); constructor.
   + specialize HP with 0 (Nat.lt_0_succ n).
     now rewrite nth_order_hd in HP.
-  + apply IHn; intros.
+  + apply IHn; intros i Hi.
     specialize HP with (S i) (proj1 (Nat.succ_lt_mono _ _) Hi).
     now rewrite <- (nth_order_tl _ _ _ _ Hi) in HP.
 Qed.
@@ -363,7 +363,7 @@ Lemma Forall2_nth_order A: forall P n (v1 v2 : t A n),
      Forall2 P v1 v2
  <-> forall i (Hi1 : i < n) (Hi2 : i < n), P (nth_order v1 Hi1) (nth_order v2 Hi2).
 Proof.
-split; induction n.
+intros P n v1 v2; split; induction n as [|n IHn].
 - intros HF i Hi1 Hi2; inversion Hi1.
 - intros HF i Hi1 Hi2.
   rewrite (eta v1), (eta v2).
@@ -382,7 +382,7 @@ split; induction n.
   rewrite (eta v1), (eta v2); constructor.
   + specialize HP with 0 (Nat.lt_0_succ _) (Nat.lt_0_succ _).
     now rewrite nth_order_hd in HP.
-  + apply IHn; intros.
+  + apply IHn; intros i Hi1 Hi2.
     specialize HP with (S i) (proj1 (Nat.succ_lt_mono _ _) Hi1)
                              (proj1 (Nat.succ_lt_mono _ _) Hi2).
     now rewrite <- (nth_order_tl _ _ _ _ Hi1), <- (nth_order_tl _ _ _ _ Hi2)  in HP.