- Optimized "auto decomp" which had a (presumably) exponential in

  the number of conjunctions to split.
- A few cleaning and uniformisation in auto.ml.
- Removal of v62 hints already in core.


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

4 files changed, 25 insertions, 25 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index beda128af..cb96f3f60 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -59,14 +59,14 @@ Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true.
 Proof.
   destruct a; destruct b; intros; split; try (reflexivity || discriminate).
 Qed.
-Hint Resolve andb_prop: bool v62.
+Hint Resolve andb_prop: bool.
 
 Lemma andb_true_intro :
   forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true.
 Proof.
   destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
 Qed.
-Hint Resolve andb_true_intro: bool v62.
+Hint Resolve andb_true_intro: bool.
 
 (** Interpretation of booleans as propositions *)
 
@@ -115,7 +115,7 @@ Inductive Empty_set : Set :=.
 
 Inductive identity (A:Type) (a:A) : A -> Type :=
   refl_identity : identity (A:=A) a a.
-Hint Resolve refl_identity: core v62.
+Hint Resolve refl_identity: core.
 
 Implicit Arguments identity_ind [A].
 Implicit Arguments identity_rec [A].
@@ -164,7 +164,7 @@ Section projections.
                               end.
 End projections. 
 
-Hint Resolve pair inl inr: core v62.
+Hint Resolve pair inl inr: core.
 
 Lemma surjective_pairing :
   forall (A B:Type) (p:A * B), p = pair (fst p) (snd p).
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 3667c4eb0..b01b80630 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -245,8 +245,8 @@ Implicit Arguments eq_ind [A].
 Implicit Arguments eq_rec [A].
 Implicit Arguments eq_rect [A].
 
-Hint Resolve I conj or_introl or_intror refl_equal: core v62.
-Hint Resolve ex_intro ex_intro2: core v62.
+Hint Resolve I conj or_introl or_intror refl_equal: core.
+Hint Resolve ex_intro ex_intro2: core.
 
 Section Logic_lemmas.
 
@@ -339,7 +339,7 @@ Proof.
   destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity.
 Qed.
 
-Hint Immediate sym_eq sym_not_eq: core v62.
+Hint Immediate sym_eq sym_not_eq: core.
 
 (** Basic definitions about relations and properties *)
 
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 8a5b195d1..322a25468 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -59,13 +59,13 @@ Proof.
   rewrite Sn_eq_Sm; trivial.
 Qed.
 
-Hint Immediate eq_add_S: core v62.
+Hint Immediate eq_add_S: core.
 
 Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
 Proof.
   red in |- *; auto.
 Qed.
-Hint Resolve not_eq_S: core v62.
+Hint Resolve not_eq_S: core.
 
 Definition IsSucc (n:nat) : Prop :=
   match n with
@@ -80,13 +80,13 @@ Proof.
   unfold not; intros n H.
   inversion H.
 Qed.
-Hint Resolve O_S: core v62.
+Hint Resolve O_S: core.
 
 Theorem n_Sn : forall n:nat, n <> S n.
 Proof.
   induction n; auto.
 Qed.
-Hint Resolve n_Sn: core v62.
+Hint Resolve n_Sn: core.
 
 (** Addition *)
 
@@ -105,7 +105,7 @@ Lemma plus_n_O : forall n:nat, n = n + 0.
 Proof.
   induction n; simpl in |- *; auto.
 Qed.
-Hint Resolve plus_n_O: core v62.
+Hint Resolve plus_n_O: core.
 
 Lemma plus_O_n : forall n:nat, 0 + n = n.
 Proof.
@@ -116,7 +116,7 @@ Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.
 Proof.
   intros n m; induction n; simpl in |- *; auto.
 Qed.
-Hint Resolve plus_n_Sm: core v62.
+Hint Resolve plus_n_Sm: core.
 
 Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m).
 Proof.
@@ -138,13 +138,13 @@ Fixpoint mult (n m:nat) {struct n} : nat :=
 
 where "n * m" := (mult n m) : nat_scope.
 
-Hint Resolve (f_equal2 mult): core v62.
+Hint Resolve (f_equal2 mult): core.
 
 Lemma mult_n_O : forall n:nat, 0 = n * 0.
 Proof.
   induction n; simpl in |- *; auto.
 Qed.
-Hint Resolve mult_n_O: core v62.
+Hint Resolve mult_n_O: core.
 
 Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m.
 Proof.
@@ -152,7 +152,7 @@ Proof.
   destruct H; rewrite <- plus_n_Sm; apply (f_equal S).
   pattern m at 1 3 in |- *; elim m; simpl in |- *; auto.
 Qed.
-Hint Resolve mult_n_Sm: core v62.
+Hint Resolve mult_n_Sm: core.
 
 (** Standard associated names *)
 
@@ -179,21 +179,21 @@ Inductive le (n:nat) : nat -> Prop :=
 
 where "n <= m" := (le n m) : nat_scope.
 
-Hint Constructors le: core v62.
-(*i equivalent to : "Hints Resolve le_n le_S : core v62." i*)
+Hint Constructors le: core.
+(*i equivalent to : "Hints Resolve le_n le_S : core." i*)
 
 Definition lt (n m:nat) := S n <= m.
-Hint Unfold lt: core v62.
+Hint Unfold lt: core.
 
 Infix "<" := lt : nat_scope.
 
 Definition ge (n m:nat) := m <= n.
-Hint Unfold ge: core v62.
+Hint Unfold ge: core.
 
 Infix ">=" := ge : nat_scope.
 
 Definition gt (n m:nat) := m < n.
-Hint Unfold gt: core v62.
+Hint Unfold gt: core.
 
 Infix ">" := gt : nat_scope.
 
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index b457a55b9..74d9726a6 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -53,7 +53,7 @@ Section Dependent_Equality.
 
   Inductive eq_dep (p:U) (x:P p) : forall q:U, P q -> Prop :=
     eq_dep_intro : eq_dep p x p x.
-  Hint Constructors eq_dep: core v62.
+  Hint Constructors eq_dep: core.
 
   Lemma eq_dep_refl : forall (p:U) (x:P p), eq_dep p x p x.
   Proof eq_dep_intro.
@@ -63,7 +63,7 @@ Section Dependent_Equality.
   Proof.
     destruct 1; auto.
   Qed.
-  Hint Immediate eq_dep_sym: core v62.
+  Hint Immediate eq_dep_sym: core.
 
   Lemma eq_dep_trans :
     forall (p q r:U) (x:P p) (y:P q) (z:P r),
@@ -135,8 +135,8 @@ Qed.
 
 (** Exported hints *)
 
-Hint Resolve eq_dep_intro: core v62.
-Hint Immediate eq_dep_sym: core v62.
+Hint Resolve eq_dep_intro: core.
+Hint Immediate eq_dep_sym: core.
 
 (************************************************************************)
 (** * Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K          *)