From 7686788688c5939e56b2a1c32aaa0336620b6170 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 30 Jan 2021 16:45:27 +0100
Subject: [PATCH] fix typos

---
 theories/typing/lib/rwlock/rwlock_code.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index c75f3fd4..2e1340a2 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -22,7 +22,7 @@ Section rwlock_functions.
     typed_val (rwlock_new ty) (fn(∅; ty) → rwlock ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (_ ret ϝ arg). inv_vec arg=>x. simpl_subst.
+      iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new (S ty.(ty_size))); [solve_typing..|].
     iIntros (r tid) "#LFT HE Hna HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -57,7 +57,7 @@ Section rwlock_functions.
     typed_val (rwlock_into_inner ty) (fn(∅; rwlock ty) → ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (_ ret ϝ arg). inv_vec arg=>x. simpl_subst.
+      iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_new ty.(ty_size)); [solve_typing..|].
     iIntros (r tid) "#LFT HE Hna HL Hk HT". simpl_subst.
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
-- 
GitLab