2 files changed, 8 insertions, 1 deletions
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index 36cdb9775..e5c9e59ee 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -12,10 +12,11 @@
 
 (** This file proposes an interface for finite maps *)
 
+(* begin hide *)
 Set Implicit Arguments.
 Unset Strict Implicit.
 Require Import FSetInterface. 
-
+(* end hide *)
 
 (** When compared with Ocaml Map, this signature has been split in two: 
    - The first part [S] contains the usual operators (add, find, ...)
@@ -204,10 +205,12 @@ Module Type S.
 	(x:key)(f:option elt->option elt'->option elt''), 
         In x (map2 f m m') -> In x m \/ In x m'.
 
+  (* begin hide *)
   Hint Immediate MapsTo_1 mem_2 is_empty_2.
   
   Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 add_3 remove_1
     remove_2 remove_3 find_1 find_2 fold_1 map_1 map_2 mapi_1 mapi_2. 
+  (* end hide *)
 
 End S.
 
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index 02a80748c..3868e84ce 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -12,10 +12,12 @@
 
 (** Set interfaces *)
 
+(* begin hide *)
 Require Export Bool.
 Require Export OrderedType.
 Set Implicit Arguments.
 Unset Strict Implicit.
+(* end hide *)
 
 (** Compatibility of a  boolean function with respect to an equality. *)
 Definition compat_bool (A:Set)(eqA: A->A->Prop)(f: A-> bool) :=
@@ -276,6 +278,7 @@ Module Type S.
   End Filter.
   End Spec.
 
+  (* begin hide *)
   Hint Immediate In_1.
   
   Hint Resolve mem_1 mem_2 equal_1 equal_2 subset_1 subset_2 empty_1
@@ -284,6 +287,7 @@ Module Type S.
     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 min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3.
+  (* end hide *)
 
 End S.