Merge PR #6934: Warn when using “Require” in a section

10 files changed, 30 insertions, 17 deletions

diff --git a/CHANGES b/CHANGES
index eaceea6dad..9dbc73adb7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -73,6 +73,7 @@ Vernacular Commands
   was removed. Use Local as a prefix instead.
 - For the Extraction Language command, "OCaml" is spelled correctly.
   The older "Ocaml" is still accepted, but deprecated.
+- Using “Require” inside a section is deprecated.
 
 Universes
 
diff --git a/library/summary.ml b/library/summary.ml
index 6ca8715559..7ef19fbfb4 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -89,6 +89,16 @@ let unfreeze_single name state =
       Pp.(seq [str "Error unfreezing summary "; str name; fnl (); CErrors.iprint e]);
     iraise e
 
+let warn_summary_out_of_scope =
+  let name = "summary-out-of-scope" in
+  let category = "dev" in
+  let default = CWarnings.Disabled in
+  CWarnings.create ~name ~category ~default (fun name ->
+    Pp.str (Printf.sprintf
+      "A Coq plugin was loaded inside a local scope (such as a Section). It is recommended to load plugins at the start of the file. Summary entry: %s"
+      name)
+    )
+
 let unfreeze_summaries ?(partial=false) { summaries; ml_module } =
   (* The unfreezing of [ml_modules_summary] has to be anticipated since it
    * may modify the content of [summaries] by loading new ML modules *)
@@ -101,7 +111,7 @@ let unfreeze_summaries ?(partial=false) { summaries; ml_module } =
     try decl.unfreeze_function String.Map.(find name summaries)
     with Not_found ->
       if not partial then begin
-        Feedback.msg_warning Pp.(str "Summary was captured out of module scope for entry " ++ str name);
+        warn_summary_out_of_scope name;
         decl.init_function ()
       end;
   in
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 543a37ff8d..f066ea462f 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -21,6 +21,7 @@ Require Import List.
 Require Import Bool.
 Require Import OrderedRing.
 Require Import Refl.
+Require Coq.micromega.Tauto.
 
 Set Implicit Arguments.
 
@@ -796,7 +797,7 @@ Definition xnormalise (t:Formula C) : list (NFormula)  :=
       | OpLe => (psub lhs rhs ,Strict) :: nil
     end.
 
-Require Import Coq.micromega.Tauto.
+Import Coq.micromega.Tauto.
 
 Definition cnf_normalise (t:Formula C) : cnf (NFormula) :=
   List.map  (fun x => x::nil) (xnormalise t).
diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index 85e2a5b235..c5a09d677e 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -30,6 +30,7 @@ Require Export Ncring_initial.
 Require Export Ncring_tac.
 Require Export Integral_domain.
 Require Import DiscrR.
+Require Import ZArith.
 
 Declare ML Module "nsatz_plugin".
 
@@ -56,9 +57,8 @@ simpl. simpl; cring.
 Qed.
 
 (* adpatation du code de Benjamin aux setoides *)
-Require Import ZArith.
-Require Export Ring_polynom.
-Require Export InitialRing.
+Export Ring_polynom.
+Export InitialRing.
 
 Definition PolZ := Pol Z.
 Definition PEZ := PExpr Z.
diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v
index db17c0d654..19b3ab397d 100644
--- a/plugins/rtauto/Rtauto.v
+++ b/plugins/rtauto/Rtauto.v
@@ -11,7 +11,7 @@
 
 Require Export List.
 Require Export Bintree.
-Require Import Bool.
+Require Import Bool BinPos.
 
 Declare ML Module "rtauto_plugin".
 
@@ -98,8 +98,6 @@ match F with
 | F_push H hyps0 F0 =>  interp_ctx hyps0 F0  ([[H]] -> G)
 end.
 
-Require Export BinPos.
-
 Ltac wipe := intros;simpl;constructor.
 
 Lemma compose0 :
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 9fd52866e3..238ac7df0b 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -28,6 +28,8 @@ intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005.
 [[Werner97]] Benjamin Werner, Sets in Types, Types in Sets, TACS, 1997.
 *)
 
+Require Import RelationClasses Logic.
+
 Set Implicit Arguments.
 Local Unset Intuition Negation Unfolding.
 
@@ -125,8 +127,6 @@ Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) :=
    formulation of choice); Note also a typo in its intended
    formulation in [[Werner97]]. *)
 
-Require Import RelationClasses Logic.
-
 Definition RepresentativeFunctionalChoice_on :=
   forall R:A->A->Prop,
     (Equivalence R) ->
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index a50140628a..a79ddead20 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -11,6 +11,7 @@
 (* G. Huet 1-9-95 *)
 
 Require Import Permut Setoid.
+Require Plus. (* comm. and ass. of plus *)
 
 Set Implicit Arguments.
 
@@ -69,9 +70,6 @@ Section multiset_defs.
     unfold meq; unfold munion; simpl; auto.
   Qed.
 
-
-  Require Plus. (* comm. and ass. of plus *)
-
   Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).
   Proof.
     unfold meq; unfold multiplicity; unfold munion.
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 95ba932324..7940bda1a7 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -13,7 +13,7 @@
 (* G. Huet 1-9-95 *)
 (* Updated Papageno 12/98 *)
 
-Require Import Bool.
+Require Import Bool Permut.
 
 Set Implicit Arguments.
 
@@ -140,8 +140,6 @@ Hint Resolve seq_right.
 (** Here we should make uniset an abstract datatype, by hiding [Charac],
     [union], [charac]; all further properties are proved abstractly *)
 
-Require Import Permut.
-
 Lemma union_rotate :
  forall x y z:uniset, seq (union x (union y z)) (union z (union x y)).
 Proof.
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 8f583be97e..d9e5ad676e 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -136,7 +136,7 @@ Section defs.
       (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
       (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) ->
       merge_lem l1 l2.
-  Require Import Morphisms.
+  Import Morphisms.
   
   Instance: Equivalence (@meq A).
   Proof. constructor; auto with datatypes. red. apply meq_trans. Defined.
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0ff6d9c17f..5779c07ab3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -805,7 +805,14 @@ let vernac_end_segment ({v=id} as lid) =
 
 (* Libraries *)
 
+let warn_require_in_section =
+  let name = "require-in-section" in
+  let category = "deprecated" in
+  CWarnings.create ~name ~category
+    (fun () -> strbrk "Use of “Require” inside a section is deprecated.")
+
 let vernac_require from import qidl =
+  if Lib.sections_are_opened () then warn_require_in_section ();
   let qidl = List.map qualid_of_reference qidl in
   let root = match from with
   | None -> None