From 12652cac427aaf49b710392fadbc06a7e32375a9 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 10 Apr 2020 19:49:54 -0400
Subject: Split off Nsatz tactic part into NsatzTactic

Closes #5445

Note that we use `Include` rather than `Export` to expose the machinery
defined in `NsatzTactic` from `Nsatz` to preserve backwards
compatibility with developments relying on absolute names of the
constants previously defined in `Nsatz.v`.
---
 test-suite/bugs/closed/bug_5445.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_5445.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_5445.v b/test-suite/bugs/closed/bug_5445.v
new file mode 100644
index 0000000000..deaf174661
--- /dev/null
+++ b/test-suite/bugs/closed/bug_5445.v
@@ -0,0 +1,11 @@
+Require Import Coq.nsatz.NsatzTactic.
+(** Ensure that loading the nsatz tactic doesn't load the reals *)
+Fail Module M := Coq.Reals.Rdefinitions.
+(** Ensure that loading the nsatz tactic doesn't load classic *)
+Fail Check Coq.Logic.Classical_Prop.classic.
+(** Ensure that this test-case hasn't messed up about the location of the reals / how to check for them *)
+Require Coq.Reals.Rdefinitions.
+Module M := Coq.Reals.Rdefinitions.
+(** Ensure that this test-case hasn't messed up about the location of classic / how to check for it *)
+Require Coq.Logic.Classical_Prop.
+Check Coq.Logic.Classical_Prop.classic.
-- 
cgit v1.2.3