diff --git a/_CoqProject b/_CoqProject index 2ba6e8277457b4a8270442bfc92a51eead1d0ea9..54a1a2d1594cda76579af944d8b8b6cc6dd24295 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 9b1d430e972ab1d850cd71c15bce7ffae7415c70..0000000000000000000000000000000000000000 --- 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 *) -(*