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/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index eefd2951f..f2555791b 100644
--- a/theories/MSets/MSetDecide.v
+++ b/theories/MSets/MSetDecide.v
@@ -15,7 +15,7 @@
 (** This file implements a decision procedure for a certain
     class of propositions involving finite sets.  *)
 
-Require Import Decidable DecidableTypeEx MSetFacts.
+Require Import Decidable Setoid DecidableTypeEx MSetFacts.
 
 (** 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 MSetLogicalFacts.
-    Require Export Decidable.
-    Require Export Setoid.
+    Export Decidable.
+    Export Setoid.
 
     (** ** Lemmas and Tactics About Decidable Propositions *)