Made option "Automatic Introduction" active by default before too many

people use the undocumented "Lemma foo x : t" feature in a way
incompatible with this activation.

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

5 files changed, 43 insertions, 43 deletions

diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index 0d24e0339..d8486180c 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -833,7 +833,7 @@ Qed.
 Instance bal_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) :
  Ok (bal l x r).
 Proof.
- intros l x r; functional induction bal l x r; intros;
+ functional induction bal l x r; intros;
  inv; repeat apply create_ok; auto; unfold create;
  (apply lt_tree_node || apply gt_tree_node); auto;
  (eapply lt_tree_trans || eapply gt_tree_trans); eauto.
@@ -894,7 +894,7 @@ Proof.
  apply create_spec.
 Qed.
 
-Instance join_ok l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r) :
+Instance join_ok : forall l x r `(Ok l, Ok r, lt_tree x l, gt_tree x r),
  Ok (join l x r).
 Proof.
  join_tac; auto with *; inv; apply bal_ok; auto;
@@ -915,10 +915,10 @@ Proof.
  rewrite bal_spec, In_node_iff, IHp, e0; simpl; intuition.
 Qed.
 
-Instance remove_min_ok l x r h `(Ok (Node l x r h)) :
+Instance remove_min_ok l x r : forall h `(Ok (Node l x r h)),
  Ok (remove_min l x r)#1.
 Proof.
- intros l x r; functional induction (remove_min l x r); simpl; intros.
+ functional induction (remove_min l x r); simpl; intros.
  inv; auto.
  assert (O : Ok (Node ll lx lr _x)) by (inv; auto).
  assert (L : lt_tree x (Node ll lx lr _x)) by (inv; auto).
@@ -958,11 +958,11 @@ Proof.
  rewrite bal_spec, remove_min_spec, e1; simpl; intuition.
 Qed.
 
-Instance merge_ok s1 s2 `(Ok s1, Ok s2)
- `(forall y1 y2 : elt, InT y1 s1 -> InT y2 s2 -> X.lt y1 y2) :
+Instance merge_ok s1 s2 : forall `(Ok s1, Ok s2)
+ `(forall y1 y2 : elt, InT y1 s1 -> InT y2 s2 -> X.lt y1 y2),
  Ok (merge s1 s2).
 Proof.
- intros s1 s2; functional induction (merge s1 s2); intros; auto;
+ functional induction (merge s1 s2); intros; auto;
  try factornode _x _x0 _x1 _x2 as s1.
  apply bal_ok; auto.
  change s2' with ((s2',m)#1); rewrite <-e1; eauto with *.
@@ -1110,11 +1110,11 @@ Proof.
  rewrite join_spec, remove_min_spec, e1; simpl; intuition.
 Qed.
 
-Instance concat_ok s1 s2 `(Ok s1, Ok s2)
- `(forall y1 y2 : elt, InT y1 s1 -> InT y2 s2 -> X.lt y1 y2) :
+Instance concat_ok s1 s2 : forall `(Ok s1, Ok s2)
+ `(forall y1 y2 : elt, InT y1 s1 -> InT y2 s2 -> X.lt y1 y2),
  Ok (concat s1 s2).
 Proof.
- intros s1 s2; functional induction (concat s1 s2); intros; auto;
+ functional induction (concat s1 s2); intros; auto;
  try factornode _x _x0 _x1 _x2 as s1.
  apply join_ok; auto.
  change (Ok (s2',m)#1); rewrite <-e1; eauto with *.
@@ -1164,7 +1164,7 @@ Proof.
  destruct (split x r); simpl in *. rewrite IHr; intuition_in; order.
 Qed.
 
-Lemma split_ok s x `{Ok s} : Ok (split x s)#l /\ Ok (split x s)#r.
+Lemma split_ok : forall s x `{Ok s}, Ok (split x s)#l /\ Ok (split x s)#r.
 Proof.
  induct s x; simpl; auto.
  specialize (IHl x).
@@ -1273,9 +1273,9 @@ Proof.
  elim_compare y x1; intuition_in.
 Qed.
 
-Instance union_ok s1 s2 `(Ok s1, Ok s2) : Ok (union s1 s2).
+Instance union_ok s1 s2 : forall `(Ok s1, Ok s2), Ok (union s1 s2).
 Proof.
- intros s1 s2; functional induction union s1 s2; intros B1 B2; auto.
+ functional induction union s1 s2; intros B1 B2; auto.
  factornode _x0 _x1 _x2 _x3 as s2; destruct_split; inv.
  apply join_ok; auto with *.
  intro y; rewrite union_spec, split_spec1; intuition_in.
@@ -1387,7 +1387,7 @@ Proof.
  rewrite H0 in H3; discriminate.
 Qed.
 
-Instance filter_ok' s acc f `(Ok s, Ok acc) :
+Instance filter_ok' : forall s acc f `(Ok s, Ok acc),
  Ok (filter_acc f acc s).
 Proof.
  induction s; simpl; auto.
@@ -1473,7 +1473,7 @@ Proof.
  intros u v H; rewrite H; auto.
 Qed.
 
-Instance partition_ok1' s acc f `(Ok s, Ok acc#1) :
+Instance partition_ok1' : forall s acc f `(Ok s, Ok acc#1),
  Ok (partition_acc f acc s)#1.
 Proof.
  induction s; simpl; auto.
@@ -1484,7 +1484,7 @@ Proof.
  apply IHs1; simpl; auto with *.
 Qed.
 
-Instance partition_ok2' s acc f `(Ok s, Ok acc#2) :
+Instance partition_ok2' : forall s acc f `(Ok s, Ok acc#2),
  Ok (partition_acc f acc s)#2.
 Proof.
  induction s; simpl; auto.
@@ -1496,10 +1496,10 @@ Proof.
 Qed.
 
 Instance partition_ok1 s f `(Ok s) : Ok (partition f s)#1.
-Proof. intros; apply partition_ok1'; auto. Qed.
+Proof. apply partition_ok1'; auto. Qed.
 
 Instance partition_ok2 s f `(Ok s) : Ok (partition f s)#2.
-Proof. intros; apply partition_ok2'; auto. Qed.
+Proof. apply partition_ok2'; auto. Qed.
 
 
 
diff --git a/theories/MSets/MSetFacts.v b/theories/MSets/MSetFacts.v
index b61bf3fe7..4e17618f7 100644
--- a/theories/MSets/MSetFacts.v
+++ b/theories/MSets/MSetFacts.v
@@ -488,13 +488,13 @@ Qed.
 
 Generalizable Variables f.
 
-Instance filter_equal `(Proper _ (E.eq==>Logic.eq) f) :
+Instance filter_equal : forall `(Proper _ (E.eq==>Logic.eq) f),
  Proper (Equal==>Equal) (filter f).
 Proof.
 intros f Hf s s' Hs a. rewrite !filter_iff, Hs by auto; intuition.
 Qed.
 
-Instance filter_subset `(Proper _ (E.eq==>Logic.eq) f) :
+Instance filter_subset : forall `(Proper _ (E.eq==>Logic.eq) f),
  Proper (Subset==>Subset) (filter f).
 Proof.
 intros f Hf s s' Hs a. rewrite !filter_iff, Hs by auto; intuition.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index b73af8f1a..45278eaf6 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -328,9 +328,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Qed.
   Hint Resolve add_inf.
 
-  Global Instance add_ok s x `(Ok s) : Ok (add x s).
+  Global Instance add_ok s x : forall `(Ok s), Ok (add x s).
   Proof.
-  intros s x; repeat rewrite <- isok_iff; revert s x.
+  repeat rewrite <- isok_iff; revert s x.
   simple induction s; simpl.
   intuition.
   intros; elim_compare x a; inv; auto.
@@ -356,9 +356,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Qed.
   Hint Resolve remove_inf.
 
-  Global Instance remove_ok s x `(Ok s) : Ok (remove x s).
+  Global Instance remove_ok s x : forall `(Ok s), Ok (remove x s).
   Proof.
-  intros s x; repeat rewrite <- isok_iff; revert s x.
+  repeat rewrite <- isok_iff; revert s x.
   induction s; simpl.
   intuition.
   intros; elim_compare x a; inv; auto.
@@ -399,9 +399,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Qed.
   Hint Resolve union_inf.
 
-  Global Instance union_ok s s' `(Ok s, Ok s') : Ok (union s s').
+  Global Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s').
   Proof.
-  intros s s'; repeat rewrite <- isok_iff; revert s s'.
+  repeat rewrite <- isok_iff; revert s s'.
   induction2; constructors; try apply @ok; auto.
   apply Inf_eq with x'; auto; apply union_inf; auto; apply Inf_eq with x; auto.
   change (Inf x' (union (x :: l) l')); auto.
@@ -426,9 +426,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Qed.
   Hint Resolve inter_inf.
 
-  Global Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s').
+  Global Instance inter_ok s s' : forall `(Ok s, Ok s'), Ok (inter s s').
   Proof.
-  intros s s'; repeat rewrite <- isok_iff; revert s s'.
+  repeat rewrite <- isok_iff; revert s s'.
   induction2.
   constructors; auto.
   apply Inf_eq with x'; auto; apply inter_inf; auto; apply Inf_eq with x; auto.
@@ -457,9 +457,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Qed.
   Hint Resolve diff_inf.
 
-  Global Instance diff_ok s s' `(Ok s, Ok s') : Ok (diff s s').
+  Global Instance diff_ok s s' : forall `(Ok s, Ok s'), Ok (diff s s').
   Proof.
-  intros s s'; repeat rewrite <- isok_iff; revert s s'.
+  repeat rewrite <- isok_iff; revert s s'.
   induction2.
   Qed.
 
@@ -644,9 +644,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   apply Inf_lt with x; auto.
   Qed.
 
-  Global Instance filter_ok s f `(Ok s) : Ok (filter f s).
+  Global Instance filter_ok s f : forall `(Ok s), Ok (filter f s).
   Proof.
-  intros s f; repeat rewrite <- isok_iff; revert s f.
+  repeat rewrite <- isok_iff; revert s f.
   simple induction s; simpl.
   auto.
   intros x l Hrec f Hs; inv.
@@ -725,9 +725,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   auto.
   Qed.
 
-  Global Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)).
+  Global Instance partition_ok1 s f : forall `(Ok s), Ok (fst (partition f s)).
   Proof.
-  intros s f; repeat rewrite <- isok_iff; revert s f.
+  repeat rewrite <- isok_iff; revert s f.
   simple induction s; simpl.
   auto.
   intros x l Hrec f Hs; inv.
@@ -735,9 +735,9 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   case (f x); case (partition f l); simpl; auto.
   Qed.
 
-  Global Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)).
+  Global Instance partition_ok2 s f : forall `(Ok s), Ok (snd (partition f s)).
   Proof.
-  intros s f; repeat rewrite <- isok_iff; revert s f.
+  repeat rewrite <- isok_iff; revert s f.
   simple induction s; simpl.
   auto.
   intros x l Hrec f Hs; inv.
diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v
index 14fe097a9..9cd28e171 100644
--- a/theories/MSets/MSetProperties.v
+++ b/theories/MSets/MSetProperties.v
@@ -947,12 +947,12 @@ Module OrdProperties (M:Sets).
 
   Instance gtb_compat x : Proper (E.eq==>Logic.eq) (gtb x).
   Proof.
-   intros x a b H. unfold gtb. rewrite H; auto.
+   intros a b H. unfold gtb. rewrite H; auto.
   Qed.
 
   Instance leb_compat x : Proper (E.eq==>Logic.eq) (leb x).
   Proof.
-   intros x a b H; unfold leb. rewrite H; auto.
+   intros a b H; unfold leb. rewrite H; auto.
   Qed.
   Hint Resolve gtb_compat leb_compat.
 
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index 8239ecef8..799e5f57e 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -275,7 +275,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   reflexivity.
   Qed.
 
-  Global Instance union_ok s s' `(Ok s, Ok s') : Ok (union s s').
+  Global Instance union_ok : forall s s' `(Ok s, Ok s'), Ok (union s s').
   Proof.
   induction s; simpl; auto; intros; inv; unfold flip; auto with *.
   Qed.
@@ -291,7 +291,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
 
   Global Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s').
   Proof.
-  unfold inter, fold, flip; intros s.
+  unfold inter, fold, flip.
   set (acc := nil (A:=elt)).
   assert (Hacc : Ok acc) by constructors.
   clearbody acc; revert acc Hacc.
@@ -322,7 +322,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   rewrite H2, <- mem_spec in H3; auto. congruence.
   Qed.
 
-  Global Instance diff_ok s s' `(Ok s, Ok s') : Ok (diff s s').
+  Global Instance diff_ok : forall s s' `(Ok s, Ok s'), Ok (diff s s').
   Proof.
   unfold diff; intros s s'; revert s.
   induction s'; simpl; unfold flip; auto; intros. inv; auto with *.
@@ -491,7 +491,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   inversion_clear H; auto.
   Qed.
 
-  Global Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)).
+  Global Instance partition_ok1 : forall s f `(Ok s), Ok (fst (partition f s)).
   Proof.
   simple induction s; simpl.
   auto.
@@ -501,7 +501,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   case (f x); case (partition f l); simpl; constructors; auto.
   Qed.
 
-  Global Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)).
+  Global Instance partition_ok2 : forall s f `(Ok s), Ok (snd (partition f s)).
   Proof.
   simple induction s; simpl.
   auto.