diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-19 12:59:35 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-19 12:59:35 -0400 |
| commit | e11bdc16ba8d0d3b92719bb9cef304a7ba52158d (patch) | |
| tree | 021a85743ea505b0a4eb7a0c3171765a2324315a /src/Util/NatUtil.v | |
| parent | e2f5be5058052be6da5d079aeda44c7d90328a11 (diff) | |
[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].
Diffstat (limited to 'src/Util/NatUtil.v')
| -rw-r--r-- | src/Util/NatUtil.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |