From c003b9733b1f11b6cc895e9c8681f0483cb193ea Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Tue, 1 Oct 2024 17:02:57 -0700
Subject: [PATCH] edit, cf #223

---
 lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fst | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fst b/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fst
index bda279eee..7143000b2 100644
--- a/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fst
+++ b/lib/pulse/lib/Pulse.Lib.MonotonicGhostRef.fst
@@ -70,9 +70,8 @@ ensures pts_to r #(f +. g) v
   unfold pts_to;
   with hg. assert (GR.pts_to r (Some g, hg));
   GR.gather r (Some f, hf) (Some g, hg);
-  let q : perm = f +. g; //annoying; can't write (f +. g) inline below
   rewrite (GR.pts_to r ((Some f, hf) `(FP.fp_pcm p).p.op` (Some g, hf)))
-       as (GR.pts_to r (Some q, hf));
+       as (GR.pts_to r (Some #perm (f +. g), hf));
   fold (pts_to r #(f +. g) v);
 }