diff --git a/progs64/verif_append2.v b/progs64/verif_append2.v
index fcf3d274c..f90abe72f 100644
--- a/progs64/verif_append2.v
+++ b/progs64/verif_append2.v
@@ -210,7 +210,7 @@ forward_if.
    iIntros "[H1 H2]".
    iIntros (cts2) "H3".
    iSpecialize ("H2" $! (a :: cts2)).
-   rewrite app_ass.
+   rewrite -app_assoc.
    iApply ("H2").
    unfold listrep at -1; fold listrep. iExists u0. iFrame.
  + (* after the loop *)
diff --git a/progs64/verif_bst.v b/progs64/verif_bst.v
index a64b4f0c7..55b267d96 100644
--- a/progs64/verif_bst.v
+++ b/progs64/verif_bst.v
@@ -312,7 +312,7 @@ Proof.
   rewrite (field_at_data_at _ t_struct_tree [StructField _left]).
   unfold treebox_rep at 1. Exists p1. cancel.
 
-  iIntros "(? & ? & ? & ? & ? & ?) Hleft".
+  iIntros "(? & ? & ? & ?) Hleft".
   clear p1.
   unfold treebox_rep.
   iExists p.
@@ -324,7 +324,7 @@ Proof.
   iFrame.
   unfold_data_at (data_at _ _ _ p).
   rewrite (field_at_data_at _ t_struct_tree [StructField _left]).
-  iFrame.
+  iStopProof; cancel.
 Qed.
 
 Lemma bst_right_entail: forall (t1 t2 t2': tree val) k (v p1 p2 p b: val),
@@ -343,7 +343,7 @@ Proof.
   rewrite (field_at_data_at _ t_struct_tree [StructField _right]).
   unfold treebox_rep at 1. Exists p2. cancel.
 
-  iIntros "(? & ? & ? & ? & ? & ?) Hright".
+  iIntros "(? & ? & ? & ?) Hright".
   clear p2.
   unfold treebox_rep.
   iExists p.
@@ -355,7 +355,7 @@ Proof.
   iFrame.
   unfold_data_at (data_at _ _ _ p).
   rewrite (field_at_data_at _ t_struct_tree [StructField _right]).
-  iFrame.
+  iStopProof; cancel.
 Qed.
 
 Lemma if_trueb: forall {A: Type} b (a1 a2: A), b = true -> (if b then a1 else a2) = a1.
@@ -823,7 +823,7 @@ Lemma subsume_insert:
 Proof.
 do_funspec_sub. destruct w as [[[b x] v] m]. simpl.
 rewrite <- fupd_intro.
-monPred.unseal. Intros.
+Intros.
 destruct args. inv H1.
 destruct args. inv H1.
 destruct args. inv H1.
@@ -842,7 +842,7 @@ Lemma subsume_treebox_new:
 Proof.
 do_funspec_sub.
 rewrite <- fupd_intro.
-monPred.unseal. Intros.
+Intros.
 Exists tt (emp : mpred). entailer!!.
 intros tau ? ?. Exists (eval_id ret_temp tau). entailer!!.
 unfold tmap_rep.
@@ -859,7 +859,7 @@ Lemma subsume_treebox_free:
 Proof.
 do_funspec_sub. destruct w as [m p]. clear H.
 rewrite <- fupd_intro.
-simpl; monPred.unseal. Intros.
+Intros.
 subst.
 unfold env_set, eval_id in *. simpl in *. 
 unfold tmap_rep.
diff --git a/progs64/verif_field_loadstore.v b/progs64/verif_field_loadstore.v
index 9f62206b5..3313c3319 100644
--- a/progs64/verif_field_loadstore.v
+++ b/progs64/verif_field_loadstore.v
@@ -1,14 +1,11 @@
 (* Do not edit this file, it was generated automatically *)
 Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.field_loadstore.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
-Section Spec.
-
-Context  `{!default_VSTGS Σ}.
-
 Definition t_struct_b := Tstruct _b noattr.
 
 Definition sub_spec (sub_id: ident) :=
@@ -73,5 +70,3 @@ Proof.
   forward.
   entailer!.
 Qed.
-
-End Spec.
diff --git a/progs64/verif_float.v b/progs64/verif_float.v
index e5ec6b24a..d751a5952 100644
--- a/progs64/verif_float.v
+++ b/progs64/verif_float.v
@@ -1,14 +1,11 @@
 (* Do not edit this file, it was generated automatically *)
 Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.float.
 
 #[export] Instance CompSpecs : compspecs.
 Proof. make_compspecs prog. Defined.
 
-Section Spec.
-
-Context  `{!default_VSTGS Σ}.
-
 Definition main_spec :=
  DECLARE _main
   WITH gv: globals
@@ -40,8 +37,8 @@ unfold data_at.
 entailer!.
 simpl.
 unfold field_at, data_at_rec, at_offset. simpl.
-  repeat (rewrite ->prop_true_andp by (auto with field_compatible)).
-fold noattr; fold tint; fold tfloat; fold tdouble. 
+  repeat (rewrite prop_true_andp by (auto with field_compatible)).
+fold noattr; fold tint; fold tfloat; fold tdouble.
 repeat match goal with |- context [field_offset ?A ?B ?C] =>
   set (aa :=field_offset A B C); compute in aa; subst aa
 end.
@@ -58,5 +55,3 @@ forward.
 forward.
 forward.
 Qed.
-
-End Spec.
\ No newline at end of file
diff --git a/progs64/verif_global.v b/progs64/verif_global.v
index 897c79ac8..133eac0a0 100644
--- a/progs64/verif_global.v
+++ b/progs64/verif_global.v
@@ -1,14 +1,11 @@
 (* Do not edit this file, it was generated automatically *)
 Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.global.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs.  mk_varspecs prog. Defined.
 
-Section Spec.
-
-Context `{!default_VSTGS Σ}.
-
 Definition h_spec :=
  DECLARE _h
   WITH gv: globals
@@ -44,5 +41,3 @@ rewrite data_at_tuint_tint.
 forward_call gv.
 forward.
 Qed.
-
-End Spec.
diff --git a/progs64/verif_incr.v b/progs64/verif_incr.v
index 9731e42d1..b1eff73a5 100644
--- a/progs64/verif_incr.v
+++ b/progs64/verif_incr.v
@@ -1,4 +1,3 @@
-(* Do not edit this file, it was generated automatically *)
 Require Import VST.concurrency.conclib.
 Require Import VST.concurrency.lock_specs.
 Require Import VST.atomics.SC_atomics.
diff --git a/progs64/verif_logical_compare.v b/progs64/verif_logical_compare.v
index f9130ff0f..f30715fb8 100644
--- a/progs64/verif_logical_compare.v
+++ b/progs64/verif_logical_compare.v
@@ -1,18 +1,18 @@
 (* Do not edit this file, it was generated automatically *)
-Require Import VST.floyd.proofauto VST.floyd.compat.
+Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.logical_compare.
-Import -(notations) compcert.lib.Maps.
 
 #[export] Instance CompSpecs : compspecs. Proof. make_compspecs prog. Defined.
 
 (****  START *)
+
 Definition logical_and_result v1 v2 : int :=
    if Int.eq v1 Int.zero then Int.zero else v2.
 
 Definition logical_or_result v1 v2 : int :=
   if Int.eq v1 Int.zero then v2 else Int.one.
 
-Print attr.
 Fixpoint quick_shortcut_logical (s: statement) : option ident :=
 match s with
 | Sifthenelse _
@@ -68,14 +68,14 @@ match s with
 end.
 
 Lemma semax_shortcut_logical:
-  forall {Espec : ext_spec unit} {cs: compspecs} Delta P Q R tid s v Qtemp Qvar GV el,
+  forall Espec {cs: compspecs} E Delta P Q R tid s v Qtemp Qvar GV el,
    quick_shortcut_logical s = Some tid ->
    typeof_temp Delta tid = Some tint ->
    local2ptree Q = (Qtemp, Qvar, nil, GV) ->
    Qtemp !! tid = None ->
    shortcut_logical (msubst_eval_expr Delta Qtemp Qvar GV) tid s = Some (v, el) ->
-   ENTAIL Delta, PROPx P (LOCALx Q (SEPx R)) ⊢ fold_right (fun e q => tc_expr Delta e ∧ q) True el ->
-   semax ⊤ Delta (PROPx P (LOCALx Q (SEPx R)))
+   ENTAIL Delta, PROPx P (LOCALx Q (SEPx R)) |-- fold_right (fun e q => tc_expr Delta e && q) TT el ->
+   semax(OK_spec := Espec)(C := cs) E Delta (PROPx P (LOCALx Q (SEPx R)))
           s (normal_ret_assert (PROPx P (LOCALx (temp tid (Vint v) :: Q) (SEPx R)))).
 Admitted.
 
diff --git a/progs64/verif_message.v b/progs64/verif_message.v
index 4cbc0511b..d02725708 100644
--- a/progs64/verif_message.v
+++ b/progs64/verif_message.v
@@ -1,5 +1,6 @@
 (* Do not edit this file, it was generated automatically *)
-Require Import VST.floyd.proofauto VST.floyd.compat.
+Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.message.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
diff --git a/progs64/verif_min.v b/progs64/verif_min.v
index 01fa269a2..9db300cd3 100644
--- a/progs64/verif_min.v
+++ b/progs64/verif_min.v
@@ -9,6 +9,7 @@
 *)
 
 Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.min.
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs.  mk_varspecs prog. Defined.
@@ -30,7 +31,7 @@ destruct H.
 subst a.
 simpl.
 apply Z.le_min_l.
-simpl. rewrite ->Z.le_min_r.
+simpl. rewrite Z.le_min_r.
 apply IHal.
 apply H.
 Qed.
@@ -78,10 +79,6 @@ Qed.
 #[export] Hint Extern 3 (is_int I32 _ (Znth _ (map Vint _))) =>
   (apply  is_int_I32_Znth_map_Vint; rewrite ?Zlength_map; lia) : core.
 
-Section Spec.
-
-Context `{!default_VSTGS Σ}.
-
 Definition minimum_spec :=
  DECLARE _minimum
   WITH a: val, n: Z, al: list Z
@@ -105,13 +102,12 @@ start_function.
 assert_PROP (Zlength al = n) by (entailer!; list_solve).
 forward.  (* min = a[0]; *)
 forward_for_simple_bound n
-  (∃ i:Z,
+  (EX i:Z,
     PROP()
     LOCAL(temp _min (Vint (Int.repr (fold_right Z.min (Znth 0 al) (sublist 0 i al))));
           temp _a a;
           temp _n (Vint (Int.repr n)))
     SEP(data_at Ews (tarray tint n) (map Vint (map Int.repr al)) a)).
-
 * (* Prove that the precondition implies the loop invariant *)
   entailer!!.
 * (* Prove that the loop body preserves the loop invariant *)
@@ -124,8 +120,8 @@ forward_for_simple_bound n
           |apply Forall_sublist; auto]).
  autorewrite with sublist.
  subst POSTCONDITION; unfold abbreviate.
- rewrite ->(sublist_split 0 i (i+1)) by lia.
- rewrite ->(sublist_one i (i+1) al) by lia.
+ rewrite (sublist_split 0 i (i+1)) by lia.
+ rewrite (sublist_one i (i+1) al) by lia.
  rewrite fold_min_another.
  forward_if.
  +
@@ -177,8 +173,8 @@ rename a0 into i.
  autorewrite with sublist.
  apply semax_post_flipped' with (Inv 1 (Z.gt n) i).
  unfold Inv.
- rewrite -> (sublist_split 0 i (i+1)) by lia.
- rewrite -> (sublist_one i (i+1) al) by lia.
+ rewrite (sublist_split 0 i (i+1)) by lia.
+ rewrite (sublist_one i (i+1) al) by lia.
  rewrite fold_min_another.
  forward_if.
  +
@@ -188,8 +184,7 @@ rename a0 into i.
  forward. (* skip; *)
  entailer!!. rewrite Z.min_l; auto; lia.
  +
- intros.
- Exists i. apply ENTAIL_refl.
+Exists i. apply ENTAIL_refl.
 *
  rename a0 into i.
  forward.
@@ -208,7 +203,7 @@ Definition minimum_spec2 :=
     PARAMS (a; Vint (Int.repr n))
     SEP   (data_at Ews (tarray tint n) (map Vint (map Int.repr al)) a)
   POST [ tint ]
-   ∃ j: Z,
+   EX j: Z,
     PROP (In j al; Forall (fun x => j<=x) al)
     RETURN (Vint (Int.repr j))
     SEP   (data_at Ews (tarray tint n) (map Vint (map Int.repr al)) a).
@@ -222,7 +217,7 @@ start_function.
 assert_PROP (Zlength al = n) by (entailer!; list_solve).
 forward.  (* min = a[0]; *)
 forward_for_simple_bound n
-  (∃ i:Z, ∃ j:Z,
+  (EX i:Z, EX j:Z,
     PROP(
          In j (sublist 0 (Z.max 1 i) al);
          Forall (Z.le j) (sublist 0 i al))
@@ -235,7 +230,7 @@ forward_for_simple_bound n
 Exists (Znth 0 al).
 autorewrite with sublist.
 entailer!!.
-rewrite -> sublist_one by lia.
+rewrite sublist_one by lia.
 constructor; auto.
 * (* Show that the loop body preserves the loop invariant *)
 Intros.
@@ -250,9 +245,9 @@ forward_if.
  forward. (* min = j; *)
  Exists (Znth i al).
  entailer!!.
- rewrite -> Z.max_r by lia.
- rewrite -> (sublist_split 0 i (i+1)) by lia.
- rewrite -> (sublist_one i (i+1) al) by lia.
+ rewrite Z.max_r by lia.
+ rewrite (sublist_split 0 i (i+1)) by lia.
+ rewrite (sublist_one i (i+1) al) by lia.
  split.
  apply in_app; right; constructor; auto.
  apply Forall_app; split.
@@ -263,23 +258,21 @@ forward_if.
  forward. (* skip; *)
  Exists j.
  entailer!!.
- rewrite -> Z.max_r by lia.
+ rewrite Z.max_r by lia.
  split.
  destruct (zlt 1 i).
- rewrite -> Z.max_r in H3 by lia.
- rewrite -> (sublist_split 0 i (i+1)) by lia.
+ rewrite Z.max_r in H3 by lia.
+ rewrite (sublist_split 0 i (i+1)) by lia.
  apply in_app; left; auto.
- rewrite -> Z.max_l in H3 by lia.
- rewrite -> (sublist_split 0 1 (i+1)) by lia.
+ rewrite Z.max_l in H3 by lia.
+ rewrite (sublist_split 0 1 (i+1)) by lia.
  apply in_app; left; auto.
- rewrite -> (sublist_split 0 i (i+1)) by lia.
+ rewrite (sublist_split 0 i (i+1)) by lia.
  apply Forall_app. split; auto.
- rewrite -> sublist_one by lia.
+ rewrite sublist_one by lia.
  repeat constructor. lia.
 * (* After the loop *)
  Intros x.
  autorewrite with sublist in *.
  forward. (* return *)
 Qed.
-
-End Spec.
\ No newline at end of file
diff --git a/progs64/verif_min64.v b/progs64/verif_min64.v
index 680de505d..f77a2407a 100644
--- a/progs64/verif_min64.v
+++ b/progs64/verif_min64.v
@@ -5,7 +5,8 @@
     forward store with 64-bit integer array subscript.
 *)
 
-Require Import VST.floyd.proofauto VST.floyd.compat.
+Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.min64.
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs.  mk_varspecs prog. Defined.
@@ -27,7 +28,7 @@ destruct H.
 subst a.
 simpl.
 apply Z.le_min_l.
-simpl. rewrite -> Z.le_min_r.
+simpl. rewrite Z.le_min_r.
 apply IHal.
 apply H.
 Qed.
diff --git a/progs64/verif_nest2.v b/progs64/verif_nest2.v
index 756d8b325..73a9ca63e 100644
--- a/progs64/verif_nest2.v
+++ b/progs64/verif_nest2.v
@@ -1,14 +1,11 @@
 (* Do not edit this file, it was generated automatically *)
 Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.nest2.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
-Section Spec.
-
-Context `{!default_VSTGS Σ}.
-
 Definition t_struct_b := Tstruct _b noattr.
 
 Definition get_spec :=
@@ -78,5 +75,3 @@ unfold_repinj.
 Time forward. (* 1.23 sec *)
 entailer!!.
 Time Qed.  (*  28 sec -> 3.45 sec *)
-
-End Spec.
diff --git a/progs64/verif_nest3.v b/progs64/verif_nest3.v
index 65310c1d8..d1dc6659e 100644
--- a/progs64/verif_nest3.v
+++ b/progs64/verif_nest3.v
@@ -1,13 +1,10 @@
 (* Do not edit this file, it was generated automatically *)
 Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.nest3.
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
-Section Spec.
-
-Context `{!default_VSTGS Σ}.
-
 Definition t_struct_c := Tstruct _c noattr.
 
 Definition get_spec0 :=
@@ -22,7 +19,7 @@ Definition get_spec0 :=
         RETURN (Vint (snd (snd (snd v))))
         SEP   (data_at Ews t_struct_c (repinj _ v) (gv _p)).
 
-Definition get_spec : ident * (@funspec Σ).
+Definition get_spec : ident * funspec.
  let t := eval compute in (reptype' t_struct_c) in
  exact (DECLARE _get
   WITH v : t, gv: globals
@@ -82,5 +79,3 @@ Time match goal with |- context [data_at _ _ ?X _] =>
 end.
 entailer!!.
 Time Qed. (* 2.74 sec *)
-
-End Spec.
diff --git a/progs64/verif_revarray.v b/progs64/verif_revarray.v
index 85ee27076..4106a2600 100644
--- a/progs64/verif_revarray.v
+++ b/progs64/verif_revarray.v
@@ -1,5 +1,6 @@
 (* Do not edit this file, it was generated automatically *)
-Require Import VST.floyd.proofauto VST.floyd.compat.
+Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.revarray.
 Require Import VST.zlist.sublist.
 
@@ -31,7 +32,7 @@ Definition flip_ends {A} lo hi (contents: list A) :=
   ++ sublist hi (Zlength contents) (rev contents).
 
 Definition reverse_Inv a0 sh contents size :=
- (∃ j:Z,
+ (EX j:Z,
   (PROP  (0 <= j; j <= size-j)
    LOCAL  (temp _a a0; temp _lo (Vint (Int.repr j)); temp _hi (Vint (Int.repr (size-j))))
    SEP (data_at sh (tarray tint size) (flip_ends j (size-j) contents) a0)))%assert.
diff --git a/progs64/verif_reverse2.v b/progs64/verif_reverse2.v
index 29a01246f..46850eaf6 100644
--- a/progs64/verif_reverse2.v
+++ b/progs64/verif_reverse2.v
@@ -1,3 +1,4 @@
+(* Do not edit this file, it was generated automatically *)
 (** Heavily annotated for a tutorial introduction. *)
 
 (** First, import the entire Floyd proof automation system, which includes
diff --git a/progs64/verif_strlib.v b/progs64/verif_strlib.v
index 84f0e7ebe..874912e80 100644
--- a/progs64/verif_strlib.v
+++ b/progs64/verif_strlib.v
@@ -1,5 +1,6 @@
 (* Do not edit this file, it was generated automatically *)
-Require Import VST.floyd.proofauto VST.floyd.compat.
+Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.strlib.
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
@@ -145,7 +146,7 @@ Lemma split_data_at_app_tschar:
                  (field_address0 (tarray tschar n) [ArraySubsc (Zlength al)] p).
 Proof.
 intros.
-apply (split2_data_at_Tarray_app _ n  sh tschar al bl ); auto.
+apply (split2_data_at_Tarray_app _ n  sh tschar al bl); auto.
 rewrite Zlength_app in H.
 change (Zlength bl = n - Zlength al); lia.
 Qed.
@@ -224,7 +225,7 @@ forward_loop (EX i : Z,
       cancel.
     assert (j = Zlength ls) by cstring; subst.
     autorewrite with sublist.
-    unfold data_at; f_equiv.
+    f_equiv.
     replace (n - (Zlength ld + Zlength ls))
      with (1 + (n - (Zlength ld + Zlength ls+1))) by rep_lia.
     rewrite <- repeat_app' by rep_lia.
@@ -532,7 +533,7 @@ forward_loop (EX i : Z,
            repeat Vundef (Z.to_nat (n - (Zlength ld + j)))) dest;
          data_at sh' (tarray tschar (Zlength ls + 1))
            (map Vbyte (ls ++ [Byte.zero])) src)).
-all: finish.
+  all: finish.
 Qed.
 
 Lemma body_strcmp: semax_body Vprog Gprog f_strcmp strcmp_spec.
diff --git a/progs64/verif_sumarray.v b/progs64/verif_sumarray.v
index e1a374321..1079b1320 100644
--- a/progs64/verif_sumarray.v
+++ b/progs64/verif_sumarray.v
@@ -1,5 +1,6 @@
 (* Do not edit this file, it was generated automatically *)
 Require Import VST.floyd.proofauto. (* Import the Verifiable C system *)
+Require Import VST.floyd.compat.
 Require Import VST.progs64.sumarray. (* Import the AST of this C program *)
 (* The next line is "boilerplate", always required after importing an AST. *)
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
@@ -14,10 +15,6 @@ Proof.
   intros. induction a; simpl; lia.
 Qed.
 
-Section Spec.
-
-Context  `{!default_VSTGS Σ}.
-
 Definition sumarray_spec : ident * funspec :=
  DECLARE _sumarray
   WITH a: val, sh : share, contents : list Z, size: Z
@@ -25,7 +22,6 @@ Definition sumarray_spec : ident * funspec :=
           PROP  (readable_share sh; 0 <= size <= Int.max_signed;
                  Forall (fun x => 0 <= x <= Int.max_unsigned) contents)
           PARAMS (a; Vint (Int.repr size))
-          GLOBALS ()
           SEP   (data_at sh (tarray tuint size) (map Vint (map Int.repr contents)) a)
   POST [ tuint ]
         PROP () LOCAL(temp ret_temp  (Vint (Int.repr (sum_Z contents))))
@@ -40,8 +36,8 @@ Definition main_spec :=
  DECLARE _main
   WITH gv : globals
   PRE  [] main_pre prog tt gv
-  POST [ tint ]  
-     PROP() 
+  POST [ tint ]
+     PROP()
      LOCAL (temp ret_temp (Vint (Int.repr (1+2+3+4)))) 
      SEP(True).
 
@@ -67,7 +63,7 @@ forward.  (* s = 0; *)
  * provide a loop invariant, so we use [forward_while] with
  * the invariant as an argument .*)
 forward_while
- (∃ i: Z,
+ (EX i: Z,
    PROP  (0 <= i <= size)
    LOCAL (temp _a a;
           temp _i (Vint (Int.repr i));
@@ -92,16 +88,16 @@ assert_PROP (Zlength contents = size). {
   entailer!. do 2 rewrite Zlength_map. reflexivity.
 }
 forward. (* x = a[i] *)
-forward. (* s += x; *) 
+forward. (* s += x; *)
 forward. (* i++; *) 
  (* Now we have reached the end of the loop body, and it's
    time to prove that the _current precondition_  (which is the
    postcondition of the loop body) entails the loop invariant. *)
- Exists (i+1).  simpl.
+ Exists (i+1).
  entailer!. simpl.
  f_equal.
- rewrite ->(sublist_split 0 i (i+1)) by lia.
- rewrite sum_Z_app. rewrite ->(sublist_one i) by lia.
+ rewrite (sublist_split 0 i (i+1)) by lia.
+ rewrite sum_Z_app. rewrite (sublist_one i) by lia.
  autorewrite with sublist. normalize.
  simpl. rewrite Z.add_0_r. reflexivity.
 * (* After the loop *)
@@ -124,7 +120,7 @@ start_function.
 rename a into gv.
 forward_call (*  s = sumarray(four,4); *)
   (gv _four, Ews,four_contents,4).
-repeat constructor; computable.
+ repeat constructor; computable.
 forward. (* return s; *)
 Qed.
 
@@ -135,5 +131,3 @@ Proof.
   semax_func_cons body_sumarray.
   semax_func_cons body_main.
 Qed.
-
-End Spec.
\ No newline at end of file
diff --git a/progs64/verif_switch.v b/progs64/verif_switch.v
index 3030c98cb..6a76ea4e9 100644
--- a/progs64/verif_switch.v
+++ b/progs64/verif_switch.v
@@ -1,34 +1,35 @@
 (* Do not edit this file, it was generated automatically *)
-Require Import VST.floyd.proofauto VST.floyd.compat.
+Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import Recdef.
 Require Import VST.progs64.switch.
-(* Require Export VST.floyd.Funspec_old_Notation. *)
+Require Export VST.floyd.Funspec_old_Notation.
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
 Definition twice_spec : ident * funspec :=
   DECLARE _twice
     WITH n : Z
-    PRE [ tint ]
+    PRE [ _n OF tint ]
       PROP  (Int.min_signed <= n+n <= Int.max_signed)
-      PARAMS (Vint (Int.repr n))
+      LOCAL (temp _n (Vint (Int.repr n)))
       SEP ()
     POST [ tint ]
       PROP ()
-      RETURN (Vint (Int.repr (n+n)))
+      LOCAL (temp ret_temp (Vint (Int.repr (n+n))))
       SEP ().
 
 
 Definition f_spec : ident * funspec :=
   DECLARE _f
     WITH x : Z
-    PRE [ tuint ]
+    PRE [ _x OF tuint ]
       PROP  (0 <= x <= Int.max_unsigned)
-      PARAMS (Vint (Int.repr x))
+      LOCAL (temp _x (Vint (Int.repr x)))
       SEP ()
     POST [ tint ]
       PROP ()
-      RETURN (Vint (Int.repr 1))
+      LOCAL (temp ret_temp (Vint (Int.repr 1)))
       SEP ().
 
 
diff --git a/progs64/verif_union.v b/progs64/verif_union.v
index f9461a46e..07870a313 100644
--- a/progs64/verif_union.v
+++ b/progs64/verif_union.v
@@ -1,11 +1,10 @@
 (* Do not edit this file, it was generated automatically *)
-Require Import VST.floyd.proofauto VST.floyd.compat.
+Require Import VST.floyd.proofauto.
+Require Import VST.floyd.compat.
 Require Import VST.progs64.union.
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
-Local Open Scope Z.
-
 Import Memdata.
 
 Definition Gprog : funspecs :=
@@ -108,7 +107,7 @@ revert k H; induction p; simpl; intros.
 rewrite Pos2Z.inj_succ in H.
 specialize (IHp (k-1)).
 spec IHp; [lia | ].
-replace (2^(k-1)) with (2^1 * 2^(k-1-1)).
+replace (2^(k-1)) with (2^1 * 2^(k-1-1))%Z.
 2:{ rewrite <- Z.pow_add_r by lia. f_equal. lia. }
 rewrite Pos2Z.inj_xI.
 lia.
@@ -116,12 +115,12 @@ lia.
 rewrite Pos2Z.inj_succ in H.
 specialize (IHp (k-1)).
 spec IHp; [lia | ].
-replace (2^(k-1)) with (2^1 * 2^(k-1-1)).
+replace (2^(k-1)) with (2^1 * 2^(k-1-1))%Z.
 2:{ rewrite <- Z.pow_add_r by lia. f_equal. lia. }
 rewrite Pos2Z.inj_xO.
 lia.
 -
-replace (2^(k-1)) with (2^1 * 2^(k-1-1)).
+replace (2^(k-1)) with (2^1 * 2^(k-1-1))%Z.
 2:{ rewrite <- Z.pow_add_r by lia. f_equal. lia. }
 change (2^1) with 2.
 assert (0 < 2 ^ (k-1-1)).