From 6d5b56d971506dfadcfc824bfbb09dc21718e42b Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 25 Dec 2014 18:13:16 +0100 Subject: Forbid Require inside interactive modules and module types. Fixes #3379 and part of #3363. Also avoids fragile code propagating required libraries when closing an interactive module. Had to fix a few occurrences in std lib. --- theories/FSets/FSetDecide.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/FSets') diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index f64df9fe1..ad067eb3d 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -15,7 +15,7 @@ (** This file implements a decision procedure for a certain class of propositions involving finite sets. *) -Require Import Decidable DecidableTypeEx FSetFacts. +Require Import Decidable Setoid DecidableTypeEx FSetFacts. (** First, a version for Weak Sets in functorial presentation *) @@ -115,8 +115,8 @@ the above form: not affect the namespace if you import the enclosing module [Decide]. *) Module FSetLogicalFacts. - Require Export Decidable. - Require Export Setoid. + Export Decidable. + Export Setoid. (** ** Lemmas and Tactics About Decidable Propositions *) -- cgit v1.2.3