Commit 797d2d16 by Ralf Jung

### Turn out Coq 8.5 already comes with a module to get lia without axioms: Lia

parent 6edb53e7
 ... @@ -21,7 +21,6 @@ prelude/listset.v ... @@ -21,7 +21,6 @@ prelude/listset.v prelude/streams.v prelude/streams.v prelude/gmap.v prelude/gmap.v prelude/base.v prelude/base.v prelude/psatz_axiomfree.v prelude/tactics.v prelude/tactics.v prelude/prelude.v prelude/prelude.v prelude/listset_nodup.v prelude/listset_nodup.v ... ...
 (** 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 *) (*
 ... @@ -3,7 +3,7 @@ ... @@ -3,7 +3,7 @@ (** This file collects general purpose tactics that are used throughout (** This file collects general purpose tactics that are used throughout the development. *) the development. *) From Coq Require Import Omega. From Coq Require Import Omega. From iris.prelude Require Export psatz_axiomfree. From Coq Require Export Lia. From iris.prelude Require Export decidable. From iris.prelude Require Export decidable. Lemma f_equal_dep {A B} (f g : ∀ x : A, B x) x : f = g → f x = g x. Lemma f_equal_dep {A B} (f g : ∀ x : A, B x) x : f = g → f x = g x. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!