bump gpfsl

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.2018-11-04.0.06dc5416") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2018-11-15.0.5b0cfc8b") | (= "dev") }
 ]

theories/typing/soundness.v

@@ -26,12 +26,12 @@ Section type_soundness.
 
   Theorem type_soundness `{typePreG Σ} (main : val) σ t :
     (∀ `{typeG Σ}, typed_val main main_type) →
-    rtc erased_step ([(main [exit_cont] at init_tview)%E], mkGB ∅ ∅ ∅) (t, σ) →
+    rtc erased_step ([(main [exit_cont] at init_tview)%E], mkGB ∅ ∅) (t, σ) →
     (* nonracing_threadpool t σ ∧ *)   (* TODO : prove DRF theorem *)
     (∀ e 𝓥, (e at 𝓥)%E ∈ t → is_Some (to_val e) ∨ reducible (e at 𝓥) σ).
   Proof.
     intros Hmain Hrtc.
-    cut (adequate NotStuck (main [exit_cont]%E at init_tview) (mkGB ∅ ∅ ∅) (λ _ _, True)).
+    cut (adequate NotStuck (main [exit_cont]%E at init_tview) (mkGB ∅ ∅) (λ _ _, True)).
     { (* split. by eapply adequate_nonracing. *)
       intros.
       edestruct (adequate_not_stuck NotStuck (main [exit_cont]%E at init_tview))
@@ -64,7 +64,7 @@ End type_soundness.
 
 Theorem type_soundness_closed (main : val) σ t :
   (∀ `{typeG typeΣ}, typed_val main main_type) →
-  rtc erased_step ([(main [exit_cont] at init_tview)%E], mkGB ∅ ∅ ∅) (t, σ) →
+  rtc erased_step ([(main [exit_cont] at init_tview)%E], mkGB ∅ ∅) (t, σ) →
   (* nonracing_threadpool t σ ∧ *)   (* TODO : prove DRF theorem *)
   (∀ e 𝓥, (e at 𝓥)%E ∈ t → is_Some (to_val e) ∨ reducible (e at 𝓥) σ).
 Proof. intros. eapply @type_soundness; try done. apply _. Qed.

theories/typing/type_context.v

@@ -56,8 +56,8 @@ Section type_context.
     eval_path p = Some v → Closed [] p.
   Proof.
     intros Hpv. revert v Hpv.
-    induction p as [| | | | |[] p IH [| | |[]| | | | | | | | | | | |] _|
-                    | | | | | | | | |]=>//.
+    induction p as [| | | | |[] p IH [| | |[]| | | | | | | | | | |] _|
+                    | | | | | | | |]=>//.
     - unfold eval_path=>? /of_to_val <-. apply is_closed_of_val.
     - simpl. destruct (eval_path p) as [[[]|]|]; intros ? [= <-].
       specialize (IH _ eq_refl). apply _.