From 797d2d1671746618ed1d38163506adc058942edd Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 29 Aug 2016 14:11:04 +0200 Subject: [PATCH] Turn out Coq 8.5 already comes with a module to get lia without axioms: Lia --- _CoqProject | 1 - prelude/psatz_axiomfree.v | 39 --------------------------------------- prelude/tactics.v | 2 +- 3 files changed, 1 insertion(+), 41 deletions(-) delete mode 100644 prelude/psatz_axiomfree.v diff --git a/_CoqProject b/_CoqProject index 2ba6e8277..54a1a2d15 100644 --- a/_CoqProject +++ b/_CoqProject @@ -21,7 +21,6 @@ prelude/listset.v prelude/streams.v prelude/gmap.v prelude/base.v -prelude/psatz_axiomfree.v prelude/tactics.v prelude/prelude.v prelude/listset_nodup.v diff --git a/prelude/psatz_axiomfree.v b/prelude/psatz_axiomfree.v deleted file mode 100644 index 9b1d430e9..000000000 --- a/prelude/psatz_axiomfree.v +++ /dev/null @@ -1,39 +0,0 @@ -(** This file is a hack that lets us use Psatz without importing all sorts of - axioms about real numbers. It has been created by copying the file - Psatz.v from the Coq distribution, removing everything defined after the lia - tactic, and removing the two lines importing RMicromega and Rdefinitions. - The original license header follows. *) - -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(*