diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 77be679070db..9984bff0c2cc 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -79,7 +79,7 @@ Register negb as core.bool.negb.
 
 (** Basic properties of [andb] *)
 
-Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true.
+Lemma andb_prop (a b:bool) : andb a b = true -> a = true /\ b = true.
 Proof.
   destruct a, b; repeat split; assumption.
 Qed.
@@ -87,8 +87,8 @@ Hint Resolve andb_prop: bool.
 
 Register andb_prop as core.bool.andb_prop.
 
-Lemma andb_true_intro :
-  forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true.
+Lemma andb_true_intro (b1 b2:bool) :
+  b1 = true /\ b2 = true -> andb b1 b2 = true.
 Proof.
   destruct b1; destruct b2; simpl; intros [? ?]; assumption.
 Qed.
@@ -245,25 +245,22 @@ End projections.
 
 Hint Resolve pair inl inr: core.
 
-Lemma surjective_pairing :
-  forall (A B:Type) (p:A * B), p = (fst p, snd p).
+Lemma surjective_pairing (A B:Type) (p:A * B) : p = (fst p, snd p).
 Proof.
   destruct p; reflexivity.
 Qed.
 
-Lemma injective_projections :
-  forall (A B:Type) (p1 p2:A * B),
+Lemma injective_projections (A B:Type) (p1 p2:A * B) :
     fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2.
 Proof.
   destruct p1; destruct p2; simpl; intros Hfst Hsnd.
   rewrite Hfst; rewrite Hsnd; reflexivity.
 Qed.
 
-Lemma pair_equal_spec :
-  forall (A B : Type) (a1 a2 : A) (b1 b2 : B),
+Lemma pair_equal_spec (A B : Type) (a1 a2 : A) (b1 b2 : B) :
     (a1, b1) = (a2, b2) <-> a1 = a2 /\ b1 = b2.
 Proof with auto.
-  split; intros.
+  split; intro H.
   - split.
     + replace a1 with (fst (a1, b1)); replace a2 with (fst (a2, b2))...
       rewrite H...
@@ -286,7 +283,7 @@ Definition prod_curry (A B C:Type) : (A -> B -> C) -> A * B -> C := uncurry.
 
 Import EqNotations.
 
-Lemma rew_pair : forall A (P Q : A->Type) x1 x2 (y1:P x1) (y2:Q x1) (H:x1=x2),
+Lemma rew_pair A (P Q : A->Type) x1 x2 (y1:P x1) (y2:Q x1) (H:x1=x2) :
   (rew H in y1, rew H in y2) = rew [fun x => (P x * Q x)%type] H in (y1,y2).
 Proof.
   destruct H. reflexivity.
@@ -347,7 +344,7 @@ Register Eq as core.comparison.Eq.
 Register Lt as core.comparison.Lt.
 Register Gt as core.comparison.Gt.
 
-Lemma comparison_eq_stable : forall c c' : comparison, ~~ c = c' -> c = c'.
+Lemma comparison_eq_stable (c c' : comparison) : ~~ c = c' -> c = c'.
 Proof.
   destruct c, c'; intro H; reflexivity || destruct H; discriminate.
 Qed.
@@ -359,12 +356,12 @@ Definition CompOpp (r:comparison) :=
     | Gt => Lt
   end.
 
-Lemma CompOpp_involutive : forall c, CompOpp (CompOpp c) = c.
+Lemma CompOpp_involutive c : CompOpp (CompOpp c) = c.
 Proof.
   destruct c; reflexivity.
 Qed.
 
-Lemma CompOpp_inj : forall c c', CompOpp c = CompOpp c' -> c = c'.
+Lemma CompOpp_inj c c' : CompOpp c = CompOpp c' -> c = c'.
 Proof.
   destruct c; destruct c'; auto; discriminate.
 Qed.
@@ -405,7 +402,7 @@ Register CompEqT as core.CompareSpecT.CompEqT.
 Register CompLtT as core.CompareSpecT.CompLtT.
 Register CompGtT as core.CompareSpecT.CompGtT.
 
-Lemma CompareSpec2Type : forall Peq Plt Pgt c,
+Lemma CompareSpec2Type Peq Plt Pgt c :
  CompareSpec Peq Plt Pgt c -> CompareSpecT Peq Plt Pgt c.
 Proof.
  destruct c; intros H; constructor; inversion_clear H; auto.
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 8f9f68a2922c..801223514381 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -523,41 +523,28 @@ Section equality_dep.
   Variable f : forall x, B x.
   Variables x y : A.
 
-  Theorem f_equal_dep : forall (H: x = y), rew H in f x = f y.
+  Theorem f_equal_dep (H: x = y) : rew H in f x = f y.
   Proof.
     destruct H; reflexivity.
   Defined.
 
 End equality_dep.
 
-Section equality_dep2.
-
-  Variable A A' : Type.
-  Variable B : A -> Type.
-  Variable B' : A' -> Type.
-  Variable f : A -> A'.
-  Variable g : forall a:A, B a -> B' (f a).
-  Variables x y : A.
-
-  Lemma f_equal_dep2 : forall {A A' B B'} (f : A -> A') (g : forall a:A, B a -> B' (f a))
-  {x1 x2 : A} {y1 : B x1} {y2 : B x2} (H : x1 = x2),
+Lemma f_equal_dep2 {A A' B B'} (f : A -> A') (g : forall a:A, B a -> B' (f a))
+  {x1 x2 : A} {y1 : B x1} {y2 : B x2} (H : x1 = x2) :
   rew H in y1 = y2 -> rew f_equal f H in g x1 y1 = g x2 y2.
-  Proof.
-    destruct H, 1. reflexivity.
-  Defined.
-
-End equality_dep2.
+Proof.
+  destruct H, 1. reflexivity.
+Defined.
 
-Lemma rew_opp_r : forall A (P:A->Type) (x y:A) (H:x=y) (a:P y), rew H in rew <- H in a = a.
+Lemma rew_opp_r A (P:A->Type) (x y:A) (H:x=y) (a:P y) : rew H in rew <- H in a = a.
 Proof.
-intros.
 destruct H.
 reflexivity.
 Defined.
 
-Lemma rew_opp_l : forall A (P:A->Type) (x y:A) (H:x=y) (a:P x), rew <- H in rew H in a = a.
+Lemma rew_opp_l A (P:A->Type) (x y:A) (H:x=y) (a:P x) : rew <- H in rew H in a = a.
 Proof.
-intros.
 destruct H.
 reflexivity.
 Defined.
@@ -597,7 +584,7 @@ Proof.
   destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity.
 Qed.
 
-Theorem f_equal_compose : forall A B C (a b:A) (f:A->B) (g:B->C) (e:a=b),
+Theorem f_equal_compose A B C (a b:A) (f:A->B) (g:B->C) (e:a=b) :
   f_equal g (f_equal f e) = f_equal (fun a => g (f a)) e.
 Proof.
   destruct e. reflexivity.
@@ -605,68 +592,69 @@ Defined.
 
 (** The groupoid structure of equality *)
 
-Theorem eq_trans_refl_l : forall A (x y:A) (e:x=y), eq_trans eq_refl e = e.
+Theorem eq_trans_refl_l A (x y:A) (e:x=y) : eq_trans eq_refl e = e.
 Proof.
   destruct e. reflexivity.
 Defined.
 
-Theorem eq_trans_refl_r : forall A (x y:A) (e:x=y), eq_trans e eq_refl = e.
+Theorem eq_trans_refl_r A (x y:A) (e:x=y) : eq_trans e eq_refl = e.
 Proof.
   destruct e. reflexivity.
 Defined.
 
-Theorem eq_sym_involutive : forall A (x y:A) (e:x=y), eq_sym (eq_sym e) = e.
+Theorem eq_sym_involutive A (x y:A) (e:x=y) : eq_sym (eq_sym e) = e.
 Proof.
   destruct e; reflexivity.
 Defined.
 
-Theorem eq_trans_sym_inv_l : forall A (x y:A) (e:x=y), eq_trans (eq_sym e) e = eq_refl.
+Theorem eq_trans_sym_inv_l A (x y:A) (e:x=y) : eq_trans (eq_sym e) e = eq_refl.
 Proof.
   destruct e; reflexivity.
 Defined.
 
-Theorem eq_trans_sym_inv_r : forall A (x y:A) (e:x=y), eq_trans e (eq_sym e) = eq_refl.
+Theorem eq_trans_sym_inv_r A (x y:A) (e:x=y) : eq_trans e (eq_sym e) = eq_refl.
 Proof.
   destruct e; reflexivity.
 Defined.
 
-Theorem eq_trans_assoc : forall A (x y z t:A) (e:x=y) (e':y=z) (e'':z=t),
+Theorem eq_trans_assoc A (x y z t:A) (e:x=y) (e':y=z) (e'':z=t) :
   eq_trans e (eq_trans e' e'') = eq_trans (eq_trans e e') e''.
 Proof.
   destruct e''; reflexivity.
 Defined.
 
-Theorem rew_map : forall A B (P:B->Type) (f:A->B) x1 x2 (H:x1=x2) (y:P (f x1)),
+Theorem rew_map A B (P:B->Type) (f:A->B) x1 x2 (H:x1=x2) (y:P (f x1)) :
   rew [fun x => P (f x)] H in y = rew f_equal f H in y.
 Proof.
   destruct H; reflexivity.
 Defined.
 
-Theorem eq_trans_map : forall {A B} {x1 x2 x3:A} {y1:B x1} {y2:B x2} {y3:B x3},
-  forall (H1:x1=x2) (H2:x2=x3) (H1': rew H1 in y1 = y2) (H2': rew H2 in y2 = y3),
+Theorem eq_trans_map {A B} {x1 x2 x3:A} {y1:B x1} {y2:B x2} {y3:B x3}
+  (H1:x1=x2) (H2:x2=x3) (H1': rew H1 in y1 = y2) (H2': rew H2 in y2 = y3) :
   rew eq_trans H1 H2 in y1 = y3.
 Proof.
-  intros. destruct H2. exact (eq_trans H1' H2').
+  destruct H2. exact (eq_trans H1' H2').
 Defined.
 
-Lemma map_subst : forall {A} {P Q:A->Type} (f : forall x, P x -> Q x) {x y} (H:x=y) (z:P x),
+Lemma map_subst {A} {P Q:A->Type} (f : forall x, P x -> Q x) {x y} (H:x=y) (z:P x) :
   rew H in f x z = f y (rew H in z).
 Proof.
   destruct H. reflexivity.
 Defined.
 
-Lemma map_subst_map : forall {A B} {P:A->Type} {Q:B->Type} (f:A->B) (g : forall x, P x -> Q (f x)),
-  forall {x y} (H:x=y) (z:P x), rew f_equal f H in g x z = g y (rew H in z).
+Lemma map_subst_map {A B} {P:A->Type} {Q:B->Type} (f:A->B) (g : forall x, P x -> Q (f x))
+  {x y} (H:x=y) (z:P x) :
+  rew f_equal f H in g x z = g y (rew H in z).
 Proof.
   destruct H. reflexivity.
 Defined.
 
-Lemma rew_swap : forall A (P:A->Type) x1 x2 (H:x1=x2) (y1:P x1) (y2:P x2), rew H in y1 = y2 -> y1 = rew <- H in y2.
+Lemma rew_swap A (P:A->Type) x1 x2 (H:x1=x2) (y1:P x1) (y2:P x2) : rew H in y1 = y2 -> y1 = rew <- H in y2.
 Proof.
   destruct H. trivial.
 Defined.
 
-Lemma rew_compose : forall A (P:A->Type) x1 x2 x3 (H1:x1=x2) (H2:x2=x3) (y:P x1),
+Lemma rew_compose A (P:A->Type) x1 x2 x3 (H1:x1=x2) (H2:x2=x3) (y:P x1) :
   rew H2 in rew H1 in y = rew (eq_trans H1 H2) in y.
 Proof.
   destruct H2. reflexivity.
@@ -674,9 +662,8 @@ Defined.
 
 (** Extra properties of equality *)
 
-Theorem eq_id_comm_l : forall A (f:A->A) (Hf:forall a, a = f a), forall a, f_equal f (Hf a) = Hf (f a).
+Theorem eq_id_comm_l A (f:A->A) (Hf:forall a, a = f a) a : f_equal f (Hf a) = Hf (f a).
 Proof.
-  intros.
   unfold f_equal.
   rewrite <- (eq_trans_sym_inv_l (Hf a)).
   destruct (Hf a) at 1 2.
@@ -684,9 +671,8 @@ Proof.
   reflexivity.
 Defined.
 
-Theorem eq_id_comm_r : forall A (f:A->A) (Hf:forall a, f a = a), forall a, f_equal f (Hf a) = Hf (f a).
+Theorem eq_id_comm_r A (f:A->A) (Hf:forall a, f a = a) a : f_equal f (Hf a) = Hf (f a).
 Proof.
-  intros.
   unfold f_equal.
   rewrite <- (eq_trans_sym_inv_l (Hf (f (f a)))).
   set (Hfsymf := fun a => eq_sym (Hf a)).
@@ -700,36 +686,36 @@ Proof.
   reflexivity.
 Defined.
 
-Lemma eq_refl_map_distr : forall A B x (f:A->B), f_equal f (eq_refl x) = eq_refl (f x).
+Lemma eq_refl_map_distr A B x (f:A->B) : f_equal f (eq_refl x) = eq_refl (f x).
 Proof.
   reflexivity.
 Qed.
 
-Lemma eq_trans_map_distr : forall A B x y z (f:A->B) (e:x=y) (e':y=z), f_equal f (eq_trans e e') = eq_trans (f_equal f e) (f_equal f e').
+Lemma eq_trans_map_distr A B x y z (f:A->B) (e:x=y) (e':y=z) : f_equal f (eq_trans e e') = eq_trans (f_equal f e) (f_equal f e').
 Proof.
 destruct e'.
 reflexivity.
 Defined.
 
-Lemma eq_sym_map_distr : forall A B (x y:A) (f:A->B) (e:x=y), eq_sym (f_equal f e) = f_equal f (eq_sym e).
+Lemma eq_sym_map_distr A B (x y:A) (f:A->B) (e:x=y) : eq_sym (f_equal f e) = f_equal f (eq_sym e).
 Proof.
 destruct e.
 reflexivity.
 Defined.
 
-Lemma eq_trans_sym_distr : forall A (x y z:A) (e:x=y) (e':y=z), eq_sym (eq_trans e e') = eq_trans (eq_sym e') (eq_sym e).
+Lemma eq_trans_sym_distr A (x y z:A) (e:x=y) (e':y=z) : eq_sym (eq_trans e e') = eq_trans (eq_sym e') (eq_sym e).
 Proof.
 destruct e, e'.
 reflexivity.
 Defined.
 
-Lemma eq_trans_rew_distr : forall A (P:A -> Type) (x y z:A) (e:x=y) (e':y=z) (k:P x),
+Lemma eq_trans_rew_distr A (P:A -> Type) (x y z:A) (e:x=y) (e':y=z) (k:P x) :
     rew (eq_trans e e') in k = rew e' in rew e in k.
 Proof.
   destruct e, e'; reflexivity.
 Qed.
 
-Lemma rew_const : forall A P (x y:A) (e:x=y) (k:P),
+Lemma rew_const A P (x y:A) (e:x=y) (k:P) :
     rew [fun _ => P] e in k = k.
 Proof.
   destruct e; reflexivity.
@@ -797,9 +783,9 @@ Lemma forall_exists_coincide_unique_domain :
   -> (exists! x, P x).
 Proof.
   intros A P H.
-  destruct H with (Q:=P) as ((x & Hx & _),_); [trivial|].
+  destruct (H P) as ((x & Hx & _),_); [trivial|].
   exists x. split; [trivial|].
-  destruct H with (Q:=fun x'=>x=x') as (_,Huniq).
+  destruct (H (fun x'=>x=x')) as (_,Huniq).
   apply Huniq. exists x; auto.
 Qed.
 
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 4ff007570ebe..1fb6dabe6fe1 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -765,7 +765,7 @@ Section Dependent_choice_lemmas.
     exists f.
     split.
     - reflexivity.
-    - induction n; simpl; apply proj2_sig.
+    - intro n; induction n; simpl; apply proj2_sig.
   Defined.
 
 End Dependent_choice_lemmas.