From aff91eaa4a304d2207e1d8914f0df183d720a7cb Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 2 Mar 2020 13:20:46 +0100
Subject: [PATCH] Generalize `or_choice_1_r`.
---
theories/examples/or.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/examples/or.v b/theories/examples/or.v
index 080b9ff..a794d2a 100644
--- a/theories/examples/or.v
+++ b/theories/examples/or.v
@@ -96,7 +96,7 @@ Section rules.
Qed.
(** Choice on the RHS *)
- Lemma or_choice_1_r (e1 e1' e2 : val) A :
+ Lemma or_choice_1_r (e1 e1' e2 : expr) A :
(REL e1 << e1' : A) -∗
REL e1 << (e1' ⊕ e2)%V : A. (* TODO: in the value scope *)
Proof.
--
GitLab