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`.
---
 doc/stdlib/hidden-files | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc/stdlib')

diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index 65c88ed8d5..3af16cb731 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -53,6 +53,7 @@ theories/micromega/ZifyComparison.v
 theories/micromega/ZifyClasses.v
 theories/micromega/ZifyPow.v
 theories/micromega/Zify.v
+theories/nsatz/NsatzTactic.v
 theories/nsatz/Nsatz.v
 theories/omega/Omega.v
 theories/omega/OmegaLemmas.v
-- 
cgit v1.2.3