From 1b258168882c17f2afed9e25d51732013bafa184 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 19 Apr 2020 12:04:43 -0400
Subject: [nsatz] Use Export rather than Include

As per https://github.com/coq/coq/pull/12073#issuecomment-612869336
---
 doc/changelog/10-standard-library/12073-split-nsatz.rst | 6 +++++-
 theories/nsatz/Nsatz.v                                  | 3 +--
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/doc/changelog/10-standard-library/12073-split-nsatz.rst b/doc/changelog/10-standard-library/12073-split-nsatz.rst
index ba6556952a..bc3c24e441 100644
--- a/doc/changelog/10-standard-library/12073-split-nsatz.rst
+++ b/doc/changelog/10-standard-library/12073-split-nsatz.rst
@@ -2,6 +2,10 @@
   It is now possible to import the :g:`nsatz` machinery without
   transitively depending on the axioms of the real numbers nor of
   classical logic by loading ``Coq.nsatz.NsatzTactic`` rather than
-  ``Coq.nsatz.Nsatz`` (fixes `#5445
+  ``Coq.nsatz.Nsatz``.  Note that some constants have changed kernel
+  names, living in ``Coq.nsatz.NsatzTactic`` rather than
+  ``Coq.nsatz.Nsatz``; this might cause minor incompatibilities that
+  can be fixed by actually running :g:`Import Nsatz` rather than
+  relying on absolute names (fixes `#5445
   <https://github.com/coq/coq/issues/5445>`_, `#12073
   <https://github.com/coq/coq/pull/12073>`_, by Jason Gross).
diff --git a/theories/nsatz/Nsatz.v b/theories/nsatz/Nsatz.v
index bdefce24f3..aa0ac144c5 100644
--- a/theories/nsatz/Nsatz.v
+++ b/theories/nsatz/Nsatz.v
@@ -33,8 +33,7 @@ Require Import DiscrR.
 Require Import ZArith.
 Require Import Lia.
 
-Require NsatzTactic.
-Include NsatzTactic.
+Require Export NsatzTactic.
 
 (* Real numbers *)
 Require Import Reals.
-- 
cgit v1.2.3