From 548d2f7c81c48eaea9460eb27052a556d134d406 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 26 Feb 2015 12:50:28 +0100
Subject: [PATCH] iris_meta comment
---
iris_meta.v | 2 ++
1 file changed, 2 insertions(+)
diff --git a/iris_meta.v b/iris_meta.v
index 47d850365..d75aa2f42 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -232,6 +232,8 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
Hypothesis fillE : forall K e, E (K [[e]]) == E e * E (K [[fork_ret]]).
(* One can prove forkE, fillE as valid internal equalities. *)
+ (* RJ: We don't have rules for internal equality of propositions, don't we? Maybe we should have an axiom,
+ saying they are equal iff they are equivalent. *)
Remark valid_intEq {P P' : Props} (H : valid(P === P')) : P == P'.
Proof. move=> w n r; exact: H. Qed.
--
GitLab