Remove v62 from stdlib.

This old compatibility hint database can be safely removed
now that coq-contribs do not depend on it anymore.

13 files changed, 43 insertions, 44 deletions

diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index 8a4bb9f42..837437a22 100644
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.v
@@ -122,4 +122,4 @@ Section Ensembles_classical.
 End Ensembles_classical.
 
  Hint Resolve Strict_super_set_contains_new_element Subtract_intro
-  not_SIncl_empty: sets v62.
+  not_SIncl_empty: sets.
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index 8d2344f93..6291248eb 100644
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -141,4 +141,4 @@ End Ensembles_facts.
 Hint Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2
   Intersection_inv Couple_inv Setminus_intro Strict_Included_intro
   Strict_Included_strict Noone_in_empty Inhabited_not_empty Add_not_Empty
-  not_Empty_Add Inhabited_add Included_Empty: sets v62.
+  not_Empty_Add Inhabited_add Included_Empty: sets.
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index 8f579214a..0fefb354b 100644
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -90,9 +90,8 @@ Section Ensembles.
 
 End Ensembles.
 
-Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: sets
-  v62.
+Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: sets.
 
 Hint Resolve Union_introl Union_intror Intersection_intro In_singleton
   Couple_l Couple_r Triple_l Triple_m Triple_r Disjoint_intro
-  Extensionality_Ensembles: sets v62.
+  Extensionality_Ensembles: sets.
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index f38dd6fdf..edbc1efec 100644
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -43,8 +43,8 @@ Section Ensembles_finis.
 
 End Ensembles_finis.
 
-Hint Resolve Empty_is_finite Union_is_finite: sets v62.
-Hint Resolve card_empty card_add: sets v62.
+Hint Resolve Empty_is_finite Union_is_finite: sets.
+Hint Resolve card_empty card_add: sets.
 
 Require Import Constructive_sets.
 
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index 34ea857d1..e74ef41e4 100644
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -200,4 +200,4 @@ Section Image.
 
 End Image.
 
-Hint Resolve Im_def image_empty finite_image: sets v62.
+Hint Resolve Im_def image_empty finite_image: sets.
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index ec38b8923..42d0c76dc 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -187,7 +187,7 @@ End multiset_defs.
 
 Unset Implicit Arguments.
 
-Hint Unfold meq multiplicity: v62 datatypes.
+Hint Unfold meq multiplicity: datatypes.
 Hint Resolve munion_empty_right munion_comm munion_ass meq_left meq_right
-  munion_empty_left: v62 datatypes.
-Hint Immediate meq_sym: v62 datatypes.
+  munion_empty_left: datatypes.
+Hint Immediate meq_sym: datatypes.
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index 3610ebce6..335fec5b0 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -51,8 +51,8 @@ Section Partial_orders.
 
 End Partial_orders.
 
-Hint Unfold Carrier_of Rel_of Strict_Rel_of: sets v62.
-Hint Resolve Definition_of_covers: sets v62.
+Hint Unfold Carrier_of Rel_of Strict_Rel_of: sets.
+Hint Resolve Definition_of_covers: sets.
 
 
 Section Partial_order_facts.
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index d636e0468..7c2435da0 100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -175,14 +175,14 @@ Qed.
 
 End The_power_set_partial_order.
 
-Hint Resolve Empty_set_minimal: sets v62.
-Hint Resolve Power_set_Inhabited: sets v62.
-Hint Resolve Inclusion_is_an_order: sets v62.
-Hint Resolve Inclusion_is_transitive: sets v62.
-Hint Resolve Union_minimal: sets v62.
-Hint Resolve Union_increases_l: sets v62.
-Hint Resolve Union_increases_r: sets v62.
-Hint Resolve Intersection_decreases_l: sets v62.
-Hint Resolve Intersection_decreases_r: sets v62.
-Hint Resolve Empty_set_is_Bottom: sets v62.
-Hint Resolve Strict_inclusion_is_transitive: sets v62.
+Hint Resolve Empty_set_minimal: sets.
+Hint Resolve Power_set_Inhabited: sets.
+Hint Resolve Inclusion_is_an_order: sets.
+Hint Resolve Inclusion_is_transitive: sets.
+Hint Resolve Union_minimal: sets.
+Hint Resolve Union_increases_l: sets.
+Hint Resolve Union_increases_r: sets.
+Hint Resolve Intersection_decreases_l: sets.
+Hint Resolve Intersection_decreases_r: sets.
+Hint Resolve Empty_set_is_Bottom: sets.
+Hint Resolve Strict_inclusion_is_transitive: sets.
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 09c90506b..e802beac9 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -90,7 +90,7 @@ Section Sets_as_an_algebra.
     apply Subtract_intro; auto with sets.
     red; intro H'1; apply H'; rewrite H'1; auto with sets.
   Qed.
-  Hint Resolve incl_soustr_add_r: sets v62.
+  Hint Resolve incl_soustr_add_r: sets.
 
   Lemma add_soustr_2 :
     forall (X:Ensemble U) (x:U),
@@ -328,9 +328,9 @@ Section Sets_as_an_algebra.
 
 End Sets_as_an_algebra.
 
-Hint Resolve incl_soustr_in: sets v62.
-Hint Resolve incl_soustr: sets v62.
-Hint Resolve incl_soustr_add_l: sets v62.
-Hint Resolve incl_soustr_add_r: sets v62.
-Hint Resolve add_soustr_1 add_soustr_2: sets v62.
-Hint Resolve add_soustr_xy: sets v62.
+Hint Resolve incl_soustr_in: sets.
+Hint Resolve incl_soustr: sets.
+Hint Resolve incl_soustr_add_l: sets.
+Hint Resolve incl_soustr_add_r: sets.
+Hint Resolve add_soustr_1 add_soustr_2: sets.
+Hint Resolve add_soustr_xy: sets.
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index 63e84199d..e9696a1ca 100644
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -254,5 +254,5 @@ Section Sets_as_an_algebra.
 End Sets_as_an_algebra.
 
 Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add
-  singlx incl_add: sets v62.
+  singlx incl_add: sets.
 
diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v
index de96fa560..45fb8134c 100644
--- a/theories/Sets/Relations_1.v
+++ b/theories/Sets/Relations_1.v
@@ -60,6 +60,6 @@ Section Relations_1.
 
 End Relations_1.
 Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains
-  same_relation: sets v62.
+  same_relation: sets.
 Hint Resolve Definition_of_preorder Definition_of_order
-  Definition_of_equivalence Definition_of_PER: sets v62.
+  Definition_of_equivalence Definition_of_PER: sets.
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v
index f1026e31a..1e0b83fe5 100644
--- a/theories/Sets/Relations_2.v
+++ b/theories/Sets/Relations_2.v
@@ -48,7 +48,7 @@ Definition Strongly_confluent : Prop :=
 
 End Relations_2.
 
-Hint Resolve Rstar_0: sets v62.
-Hint Resolve Rstar1_0: sets v62.
-Hint Resolve Rstar1_1: sets v62.
-Hint Resolve Rplus_0: sets v62.
+Hint Resolve Rstar_0: sets.
+Hint Resolve Rstar1_0: sets.
+Hint Resolve Rstar1_1: sets.
+Hint Resolve Rplus_0: sets.
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index 92b299885..c05b5ee76 100644
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.v
@@ -51,10 +51,10 @@ Section Relations_3.
    Definition Noetherian : Prop := forall x:U, noetherian x.
 
 End Relations_3.
-Hint Unfold coherent: sets v62.
-Hint Unfold locally_confluent: sets v62.
-Hint Unfold confluent: sets v62.
-Hint Unfold Confluent: sets v62.
-Hint Resolve definition_of_noetherian: sets v62.
-Hint Unfold Noetherian: sets v62.
+Hint Unfold coherent: sets.
+Hint Unfold locally_confluent: sets.
+Hint Unfold confluent: sets.
+Hint Unfold Confluent: sets.
+Hint Resolve definition_of_noetherian: sets.
+Hint Unfold Noetherian: sets.