Cleanup attempt of Hints in *Interface.v files.

See recent discussion in coq-club.



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

1 files changed, 17 insertions, 10 deletions

diff --git a/theories/FSets/FSetWeakInterface.v b/theories/FSets/FSetWeakInterface.v
index 72084d0340..3079ec8719 100644
--- a/theories/FSets/FSetWeakInterface.v
+++ b/theories/FSets/FSetWeakInterface.v
@@ -12,8 +12,7 @@
 
 (** Set interfaces for types with only a decidable equality, but no ordering *)
 
-Require Export Bool.
-Require Export DecidableType.
+Require Export Bool DecidableType.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -229,13 +228,21 @@ Module Type S.
 
   End Spec.
 
-  Hint Immediate In_1.
-  
-  Hint Resolve mem_1 mem_2 equal_1 equal_2 subset_1 subset_2 empty_1
-    is_empty_1 is_empty_2 choose_1 choose_2 add_1 add_2 add_3 remove_1
-    remove_2 remove_3 singleton_1 singleton_2 union_1 union_2 union_3 inter_1
-    inter_2 inter_3 diff_1 diff_2 diff_3 filter_1 filter_2 filter_3 for_all_1
-    for_all_2 exists_1 exists_2 partition_1 partition_2 elements_1 elements_2
-    elements_3.
+  Hint Resolve mem_1 equal_1 subset_1 empty_1
+    is_empty_1 choose_1 choose_2 add_1 add_2 remove_1
+    remove_2 singleton_2 union_1 union_2 union_3
+    inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1
+    partition_1 partition_2 elements_1 elements_3 
+    : set.
+  Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3
+    remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2
+    filter_1 filter_2 for_all_2 exists_2 elements_2 
+    : set.
+  (* for compatibility with earlier hints *)
+  Hint Resolve In_1 mem_2 equal_2 subset_2 is_empty_2 add_3
+    remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2
+    filter_1 filter_2 for_all_2 exists_2 elements_2 
+    : oldset.
+
 
 End S.