From f2e4416cf1ec7f3a3b21750d3a124461100a2fa3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 4 Dec 2020 17:40:35 +0100
Subject: [PATCH] use unicode and coqdoc

---
 iris_heap_lang/proofmode.v | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 9dc2d4622..8d25b14b8 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -62,20 +62,21 @@ Proof. rewrite envs_entails_eq=> ->. by rewrite twp_value_fupd. Qed.
 
 Ltac wp_expr_simpl := wp_expr_eval simpl.
 
+(** Simplify the goal if it is [WP] of a value.
+  If the postcondition already allows a fupd, do not add a second one.
+  But otherwise, *do* add a fupd. This ensures that all the lemmas applied
+  here are bidirectional, so we never will make a goal unprovable. *)
 Ltac wp_value_head :=
   lazymatch goal with
-  (* If the postcondition already allows a fupd, do not add a second one.
-     But otherwise, *do* add a fupd. This ensures that all the lemmas applied
-     here are bidirectional, so we never will make a goal unprovable. *)
-  | |- envs_entails _ (wp ?s ?E (Val _) (fun _ => fupd ?E _ _)) =>
+  | |- envs_entails _ (wp ?s ?E (Val _) (λ _, fupd ?E _ _)) =>
       eapply tac_wp_value_nofupd
-  | |- envs_entails _ (wp ?s ?E (Val _) (fun _ => wp _ ?E _ _)) =>
+  | |- envs_entails _ (wp ?s ?E (Val _) (λ _, wp _ ?E _ _)) =>
       eapply tac_wp_value_nofupd
   | |- envs_entails _ (wp ?s ?E (Val _) _) =>
       eapply tac_wp_value
-  | |- envs_entails _ (twp ?s ?E (Val _) (fun _ => fupd ?E _ _)) =>
+  | |- envs_entails _ (twp ?s ?E (Val _) (λ _, fupd ?E _ _)) =>
       eapply tac_twp_value_nofupd
-  | |- envs_entails _ (twp ?s ?E (Val _) (fun _ => twp _ ?E _ _)) =>
+  | |- envs_entails _ (twp ?s ?E (Val _) (λ _, twp _ ?E _ _)) =>
       eapply tac_twp_value_nofupd
   | |- envs_entails _ (twp ?s ?E (Val _) _) =>
       eapply tac_twp_value
-- 
GitLab