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.

1 files changed, 3 insertions, 3 deletions

diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index f64df9fe1e..ad067eb3d8 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 *)