From e11bdc16ba8d0d3b92719bb9cef304a7ba52158d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 19 Jun 2017 12:59:35 -0400 Subject: [Require NatUtil] should not change [tauto] Work around [bug #5444](https://coq.inria.fr/bugs/show_bug.cgi?id=5444), [Require Nsatz] should not change the behavior of [tauto]. Because [tauto] is stupid and checks to see whether or not [Classical_Prop] has been *required* to decide whether or not to use classical axioms. Aren't side-effects of [Require] wonderful? Since we're not actually using nsatz or psatz in NatUtil, we now simply [Require Import Lia]. --- src/Util/NatUtil.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util/NatUtil.v') diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 80169c784..087f0a6c7 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -1,6 +1,6 @@ Require Coq.Logic.Eqdep_dec. Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega. -Require Import Coq.micromega.Psatz. +Require Import Coq.micromega.Lia. Import Nat. Scheme Equality for nat. -- cgit v1.2.3