aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-03-29 08:31:28 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-03-29 08:31:28 +0000
commitf4c41760e935836315cb26f165d2c720cfbf89cb (patch)
treeaddbd85ccd4e1cd7c73090854e015e33168ac5cc /theories/FSets
parentb730066fb4dfdeccd7b17538eda845d0048c68ca (diff)
pour coqdoc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8671 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets')
-rw-r--r--theories/FSets/FMapInterface.v5
-rw-r--r--theories/FSets/FSetInterface.v4
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.