From d3414f13f192af3a4e696ae0538e95d6094c9bc9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 5 Jun 2018 10:42:51 +0200
Subject: [PATCH] use unicode
---
theories/base_logic/bi.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index c1b8e8f25..46e434466 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -51,7 +51,7 @@ Proof.
- exact: persistently_mono.
- exact: persistently_idemp_2.
- (* emp ⊢ <pers> emp (ADMISSIBLE) *)
- trans (uPred_forall (M:=M) (fun _ : False => uPred_persistently uPred_emp)).
+ trans (uPred_forall (M:=M) (λ _ : False, uPred_persistently uPred_emp)).
+ apply forall_intro=>[[]].
+ etrans; first exact: persistently_forall_2.
apply persistently_mono. exact: pure_intro.
@@ -111,7 +111,7 @@ Proof.
- exact: plainly_impl_plainly.
- (* P ⊢ ■emp (ADMISSIBLE) *)
intros P.
- trans (uPred_forall (M:=M) (fun _ : False => uPred_plainly uPred_emp)).
+ trans (uPred_forall (M:=M) (λ _ : False , uPred_plainly uPred_emp)).
+ apply forall_intro=>[[]].
+ etrans; first exact: plainly_forall_2.
apply plainly_mono. exact: pure_intro.
--
GitLab