From 28e9d3458caa99afbe747e9cacd38f45d333b0af Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 24 Mar 2015 13:44:42 +0100
Subject: [PATCH] move axiom to its own file
---
lib/ModuRes/Axioms.v | 4 ++++
lib/ModuRes/RAConstr.v | 9 ++-------
2 files changed, 6 insertions(+), 7 deletions(-)
create mode 100644 lib/ModuRes/Axioms.v
diff --git a/lib/ModuRes/Axioms.v b/lib/ModuRes/Axioms.v
new file mode 100644
index 000000000..a9c911718
--- /dev/null
+++ b/lib/ModuRes/Axioms.v
@@ -0,0 +1,4 @@
+(* This file defines all axioms we are relying on in our development. *)
+
+Axiom ProofIrrelevance: forall (P: Prop) (p q: P), p = q.
+Ltac pi p q := erewrite (ProofIrrelevance _ p q).
diff --git a/lib/ModuRes/RAConstr.v b/lib/ModuRes/RAConstr.v
index 376023711..7677865f6 100644
--- a/lib/ModuRes/RAConstr.v
+++ b/lib/ModuRes/RAConstr.v
@@ -1,5 +1,5 @@
Require Import Ssreflect.ssreflect Ssreflect.ssrfun Omega.
-Require Import PreoMet RA.
+Require Import PreoMet RA Axioms.
Local Open Scope ra_scope.
Local Open Scope predom_scope.
@@ -331,13 +331,8 @@ Section Agreement.
end.
Local Ltac ra_ag_destr := repeat (match goal with [ x : ra_agree |- _ ] => destruct x end).
-
- (* Land of dragons starts here *)
- Axiom ProofIrrelevance: forall (P: Prop) (p q: P), p = q.
- Ltac pi p q := erewrite (ProofIrrelevance _ p q).
-
Local Ltac ra_ag_auto := first [by firstorder | split; [by firstorder|intros pv1 pv2; pi pv1 pv2; by firstorder ]].
-
+
Global Instance ra_agree_eq_equiv : Equivalence ra_agree_eq.
Proof.
split; repeat intro; ra_ag_destr; try (exact I || contradiction); [| |]. (* 3 goals left. *)
--
GitLab