From 0cdfa2fb137989f75cdebfa3a64726bc0d56a8af Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 6 Jun 2008 17:00:52 +0000
Subject: avoid duplicated creation of WFacts instances

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11064 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/FSets/FSetDecide.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'theories/FSets/FSetDecide.v')

diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index e8d639003b..fe6623c339 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -22,6 +22,7 @@ Require Import Decidable DecidableTypeEx FSetFacts.
 (** First, a version for Weak Sets *)
 
 Module WDecide (E : DecidableType)(Import M : WSfun E).
+ Module F := FSetFacts.WFacts E M.
 
 (** * Overview
     This functor defines the tactic [fsetdec], which will
@@ -462,7 +463,7 @@ the above form:
         the predicates [In] and [E.eq] applied only to
         variables.  We are going to use them with [autorewrite].
         *)
-    Module F := FSetFacts.WFacts E M.
+
     Hint Rewrite
       F.empty_iff F.singleton_iff F.add_iff F.remove_iff
       F.union_iff F.inter_iff F.diff_iff
-- 
cgit v1.2.3