From 4d3ecf1acd584200fe4299b8d12104c7acc33579 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 4 Dec 2018 11:31:39 -0500
Subject: Revert "Add subst to the end of nia in the test-suite"

This reverts commit b49f4e966443a76ac70d37c4cde68f94de164c01.

It turns out the 4x was due to .nia.cache (because I didn't clean
sufficiently in testing), not due to `subst`.
---
 test-suite/success/Nia.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v
index c157173b77..6cb645d9eb 100644
--- a/test-suite/success/Nia.v
+++ b/test-suite/success/Nia.v
@@ -4,7 +4,7 @@ Open Scope Z_scope.
 
 (** Add [Z.div_mod_to_quot_rem] to the end of [zify], just for this
     file. *)
-Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem; subst.
+Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.div_mod_to_quot_rem.
 
 Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed.
 Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed.
-- 
cgit v1.2.3