diff --git a/opam b/opam
index e4fc5bc7b5afaa9418d5e4857f208500dc3c0e01..875c0e1477675ae39aad1e7f9fbfa27fa172438b 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.2019-12-10.0.c3e8211e") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2019-12-16.1.573302f9") | (= "dev") }
 ]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index 1696ed6e9be56a0a6b632e6400de61da1185a719..426e806aa56510f446ff2011e3386e4db57fccd7 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -290,8 +290,8 @@ Section arc.
     Proper (pointwise_relation _ (dist n) ==> dist n ==>
                 eq ==> eq ==> eq ==> eq ==> eq ==> dist n) arc_inv.
   Proof.
-    move => ?????????????????????. subst.
-    apply bi.sep_ne; [done|]. apply bi.sep_ne; apply GPS_INV_ne.
+    repeat intro. subst.
+    apply bi.sep_ne; [done|]. apply bi.sep_ne; apply GPS_INV_ne; [|done| |done].
     - move => b ?????. apply bi.exist_ne => st.
       apply bi.sep_ne; [done|]. destruct b; [|done]. apply bi.sep_ne; [done|].
       destruct st as [[]|]; [|done]. solve_proper.
@@ -305,7 +305,7 @@ Section arc.
                 eq ==> eq ==> eq ==> eq ==> eq ==> (≡))
            arc_inv.
   Proof.
-    move => ?????????????????????. subst.
+    repeat intro. subst.
     apply bi.sep_proper; [done|].
     apply bi.sep_proper; apply GPS_INV_proper; auto;
     move => b ?????; apply bi.exist_proper => ?; solve_proper.
@@ -316,7 +316,7 @@ Section arc.
                          eq ==> eq ==> eq ==> eq ==> eq ==> eq ==> dist n)
            is_arc.
   Proof.
-    move => ????????????????????????. subst. constructor => ?.
+    repeat intro. subst. constructor => ?.
     rewrite /is_arc. apply view_inv_contractive.
     destruct n; [done|by apply arc_inv_ne].
   Qed.
@@ -325,7 +325,7 @@ Section arc.
     Proper (pointwise_relation _ (≡) ==> (≡) ==> eq
                 ==> eq ==> eq ==> eq ==> eq ==> eq ==> (≡)) is_arc.
   Proof.
-    move => ????????????????????????. subst.
+    repeat intro. subst.
     by apply view_inv_proper, arc_inv_proper.
   Qed.
 
diff --git a/theories/lang/spawn.v b/theories/lang/spawn.v
index 7ef91fc46840adf62b653376dae14976054bdc78..19a617f90082b9c50e279e0d3a28ab6b426c6749 100644
--- a/theories/lang/spawn.v
+++ b/theories/lang/spawn.v
@@ -75,7 +75,7 @@ Global Instance finish_handle_contractive n γc γe c :
 Proof.
   move => ???. do 3 (apply bi.exist_ne => ?).
   apply bi.sep_ne; [done|]. apply bi.sep_ne; [|done].
-  apply GPS_vSP_Writer_contractive. destruct n; [done|].
+  apply GPS_vSP_Writer_contractive; [|done]. destruct n; [done|].
   simpl => ??????. apply bi.exist_ne => b'.
   apply bi.sep_ne; [done|]. destruct b'; [|done]. solve_proper.
 Qed.