From 7e38b6627caaab7d19c4fc0ee542a67d9f8970c2 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 24 Oct 2016 17:28:51 +0200 Subject: Remove v62 from stdlib. This old compatibility hint database can be safely removed now that coq-contribs do not depend on it anymore. --- theories/Sets/Classical_sets.v | 2 +- theories/Sets/Constructive_sets.v | 2 +- theories/Sets/Ensembles.v | 5 ++--- theories/Sets/Finite_sets.v | 4 ++-- theories/Sets/Image.v | 2 +- theories/Sets/Multiset.v | 6 +++--- theories/Sets/Partial_Order.v | 4 ++-- theories/Sets/Powerset.v | 22 +++++++++++----------- theories/Sets/Powerset_Classical_facts.v | 14 +++++++------- theories/Sets/Powerset_facts.v | 2 +- theories/Sets/Relations_1.v | 4 ++-- theories/Sets/Relations_2.v | 8 ++++---- theories/Sets/Relations_3.v | 12 ++++++------ 13 files changed, 43 insertions(+), 44 deletions(-) (limited to 'theories/Sets') 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. -- cgit v1.2.3