From 261714ad9f8aaecde6a217926d07bcba6e8ebf30 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 10 Dec 2018 10:36:37 +0100
Subject: [PATCH] A comment about `later_car` not being non-expansive.
---
theories/algebra/ofe.v | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 716350954..facbfd82b 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -984,6 +984,10 @@ Proof.
Qed.
(** Later *)
+(** Note that the projection [later_car] is not non-expansive (see also the
+lemma [later_car_anti_contractive] below), so it cannot be used in the logic.
+If you need to get a witness out, you should use the lemma [Next_uninj]
+instead. *)
Record later (A : Type) : Type := Next { later_car : A }.
Add Printing Constructor later.
Arguments Next {_} _.
--
GitLab