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.

3 files changed, 7 insertions, 8 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 *)
 
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index eefd2951ff..f2555791b2 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 *)
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index c483b1d833..25ea6b7269 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -11,6 +11,7 @@
 Require Import Coq.Init.Wf.
 Require Import Coq.Program.Utils.
 Require Import ProofIrrelevance.
+Require Import FunctionalExtensionality.
 
 Local Open Scope program_scope.
 
@@ -221,8 +222,6 @@ Ltac fold_sub f :=
 
 Module WfExtensionality.
 
-  Require Import FunctionalExtensionality.
-
   (** The two following lemmas allow to unfold a well-founded fixpoint definition without
      restriction using the functional extensionality axiom. *)