aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FMapPositive.v
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-09-26 11:18:22 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-09-26 11:18:22 +0000
commit351a500eada776832ac9b09657e42f5d6cd7210f (patch)
treeaf45a745540e1154eab8955c17e03cbbe2e6b878 /theories/FSets/FMapPositive.v
parent5155de9ee4bd01127a57c36cebbd01c5d903d048 (diff)
mise a jour du nouveau ring et ajout du nouveau field, avant renommages
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets/FMapPositive.v')
-rw-r--r--theories/FSets/FMapPositive.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 9008b3623..10f6d44f3 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -13,6 +13,7 @@
(* $Id$ *)
+Require Import Bool.
Require Import ZArith.
Require Import OrderedType.
Require Import FMapInterface.