diff --git a/gpfsl-examples/queue/proof_hw_graph.v b/gpfsl-examples/queue/proof_hw_graph.v
index c2dbb52ec373b83dd25a3cc4e927ad3a837399c3..1781c51bc8787631c6280250141d7870ea4ee523 100644
--- a/gpfsl-examples/queue/proof_hw_graph.v
+++ b/gpfsl-examples/queue/proof_hw_graph.v
@@ -858,7 +858,7 @@ Proof.
     rewrite singleton_op. f_equiv. }
   split; last first. { rewrite /= !left_id right_id. by apply auth_auth_valid. }
   split.
-  { rewrite /= -!pair_op !left_id !right_id /=. split; [done|].
+  { rewrite /= -!pair_op /= left_id !right_id /=. split; [done|].
     apply mono_nat_auth_valid. }
   rewrite /= !left_id. apply auth_both_valid_discrete. clear. subst slots.
   move : 0%nat.
diff --git a/gpfsl-examples/sflib.v b/gpfsl-examples/sflib.v
index 14b6cb9c06186b5752658c599404179d4edac1aa..8dc7a20985602fa6a30eea2bcf498e8d0dc41f8e 100644
--- a/gpfsl-examples/sflib.v
+++ b/gpfsl-examples/sflib.v
@@ -786,14 +786,6 @@ Ltac clear_upto H :=
 
 Definition _Evar_sflib_ (A:Type) (x:A) := x.
 
-Tactic Notation "hide_evar" int_or_var(n) := let QQ := fresh "QQ" in
-  hget_evar n; intro;
-  lazymatch goal with [ H := ?X |- _] =>
-    set (QQ := X) in *; fold (_Evar_sflib_ X) in QQ; clear H
-  end.
-
-Ltac hide_evars := repeat (hide_evar 1).
-
 Ltac show_evars := repeat (match goal with [ H := @_Evar_sflib_ _ _ |- _ ] => unfold
  _Evar_sflib_ in H; unfold H in *; clear H end).
 
diff --git a/orc11/location.v b/orc11/location.v
index 0625a579dd23567f155333f74e1a3bbfcc53ce94..b814262fd0ec3d1f45e707ddc472b1090a5adf90 100644
--- a/orc11/location.v
+++ b/orc11/location.v
@@ -160,7 +160,7 @@ Lemma shift_lblock_0 l : l >> 0 = l.
 Proof. apply shift_0. Qed.
 
 Global Instance shift_lblock_inj l : Inj (=) (=) (l >>).
-Proof. destruct l as [b o]; intros n n' [=?]; lia. Qed.
+Proof. destruct l as [b o]; move => n n' []; lia. Qed.
 
 Lemma shift_lblock l n : (l >> n).1 = l.1.
 Proof. done. Qed.
diff --git a/orc11/memory.v b/orc11/memory.v
index 1df257912ae921558733bd0cb488edff76e7e9c8..332b90aea1bad2331635cffc1f46d094baf4397b 100644
--- a/orc11/memory.v
+++ b/orc11/memory.v
@@ -867,7 +867,7 @@ Section Memory.
     etrans; first by apply SUB.
     move => [l t]. case Eq : (M1 !! (l,t))=> [m|].
     + by rewrite (lookup_mem_addins_old _ _ _ _ _ _ Eq ADD).
-    + by case (M2 !! (l, t)).
+    + simpl. by case_match.
   Qed.
 
 
@@ -1518,7 +1518,7 @@ Section Memory.
       cell_list' l n M Cl = cell_list' l n M [] ++ Cl.
     Proof.
       revert Cl. induction n as [|n Hn] => Cl /=; first done.
-      rewrite /cell_cons Hn (Hn [_]) app_assoc_reverse //.
+      rewrite /cell_cons Hn (Hn [_]) -app_assoc //.
     Qed.
 
     Lemma cell_list'_cons l (n: nat) M Cl C: