From bc5e42d95c86f33e5caa65c82721fc9b2ddc4042 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 13 Feb 2020 10:09:31 +0100
Subject: [PATCH] bump GPFSL

---
 .gitignore                               |  1 +
 opam                                     |  2 +-
 theories/typing/examples/nonlexical.v    |  2 +-
 theories/typing/function.v               | 10 +++++-----
 theories/typing/lib/rwlock/rwlock_code.v |  2 +-
 5 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/.gitignore b/.gitignore
index 3816b70d..b334242b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -12,6 +12,7 @@
 build-dep/
 Makefile.coq
 Makefile.coq.conf
+.Makefile.coq.d
 .coqdeps.d
 _opam
 *.crashcoqide
diff --git a/opam b/opam
index 6defee7d..3916574c 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2020-02-11.1.5b5497be") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2020-02-12.0.119dcc0b") | (= "dev") }
 ]
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index 6a26e7bf..4f7623e2 100644
--- a/theories/typing/examples/nonlexical.v
+++ b/theories/typing/examples/nonlexical.v
@@ -87,7 +87,7 @@ Section non_lexical.
       iApply type_endlft.
       iApply (type_cont [_] [ϝ ⊑ₗ []]
             (λ r, [o ◁ box (Π[uninit 1;uninit 1]); map ◁ box (uninit 1);
-                   key ◁ box K; r!!!0 ◁ box (&uniq{m} V)])).
+                   key ◁ box K; (r!!!0%fin:val) ◁ box (&uniq{m} V)])).
       { iIntros (k). simpl_subst.
         iApply type_case_own;
           [solve_typing| constructor; [|constructor; [|constructor]]; left].
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 30516b68..46c8d61c 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -25,7 +25,7 @@ Section fn.
          ⌜vl = [@RecV fb (kb::xb) e H]⌝ ∗ ⌜length xb = n⌝ ∗
          ▷ ∀ (x : A) (ϝ : lft) (k : val) (xl : vec val (length xb)),
             □ typed_body ((fp x).(fp_E)  ϝ) [ϝ ⊑ₗ []]
-                         [k◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
+                         [k◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [(v!!!0%fin:val) ◁ box (fp x).(fp_ty)])]
                          (zip_with (TCtx_hasty ∘ of_val) xl
                                    (box <$> (vec_to_list (fp x).(fp_tys))))
                          (subst_v (fb::kb::xb) (RecV fb (kb::xb) e:::k:::xl) e))%I |}.
@@ -323,7 +323,7 @@ Section typing.
                    {A} (fp : A → fn_params (length ps)) (k : val) x :
     Forall (lctx_lft_alive E L) κs →
     (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) L ((fp x).(fp_E) ϝ)) →
-    typed_body E L [k ◁cont(L, λ v : vec _ 1, (v!!!0 ◁ box (fp x).(fp_ty)) :: T)]
+    typed_body E L [k ◁cont(L, λ v : vec _ 1, ((v!!!0%fin:val) ◁ box (fp x).(fp_ty)) :: T)]
                ((p ◁ fn fp) ::
                 zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)) ++
                 T)
@@ -371,7 +371,7 @@ Section typing.
     typed_body E L C T (letcall: b := p ps in e).
   Proof.
     iIntros (?? Hpsc ????) "He".
-    iApply (type_cont_norec [_] _ (λ r, (r!!!0 ◁ box (fp x).(fp_ty)) :: T')).
+    iApply (type_cont_norec [_] _ (λ r, ((r!!!0%fin:val) ◁ box (fp x).(fp_ty)) :: T')).
     - (* TODO : make [solve_closed] work here. *)
       eapply is_closed_weaken; first done. set_solver+.
     - (* TODO : make [solve_closed] work here. *)
@@ -400,7 +400,7 @@ Section typing.
     n = length argsb →
     □ (∀ x ϝ (f : val) k (args : vec val (length argsb)),
           typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ₗ []]
-                     [k ◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
+                     [k ◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [(v!!!0%fin:val) ◁ box (fp x).(fp_ty)])]
                      ((f ◁ fn fp) ::
                         zip_with (TCtx_hasty ∘ of_val) args
                                  (box <$> vec_to_list (fp x).(fp_tys)) ++ T)
@@ -423,7 +423,7 @@ Section typing.
     n = length argsb →
     □ (∀ x ϝ k (args : vec val (length argsb)),
         typed_body ((fp x).(fp_E) ϝ) [ϝ ⊑ₗ []]
-                   [k ◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [v!!!0 ◁ box (fp x).(fp_ty)])]
+                   [k ◁cont([ϝ ⊑ₗ []], λ v : vec _ 1, [(v!!!0%fin:val) ◁ box (fp x).(fp_ty)])]
                    (zip_with (TCtx_hasty ∘ of_val) args
                              (box <$> vec_to_list (fp x).(fp_tys)) ++ T)
                    (subst_v (BNamed "return" :: argsb) (k ::: args) e)) -∗
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index a9367fe5..7acb5a20 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -335,7 +335,7 @@ Section rwlock_functions.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iApply (type_cont [_] [ϝ ⊑ₗ []] (λ r, [x ◁ box (&shr{α}(rwlock ty));
-                                        r!!!0 ◁ box (option (rwlockwriteguard α ty))]));
+                                        (r!!!0%fin:val) ◁ box (option (rwlockwriteguard α ty))]));
       [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
       simpl_subst; last first.
     { iApply type_delete; [solve_typing..|]. iApply type_jump; solve_typing. }
-- 
GitLab