diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
index 860809b30..4444aba9c 100644
--- a/.github/workflows/coq-action.yml
+++ b/.github/workflows/coq-action.yml
@@ -23,6 +23,7 @@ jobs:
           # See https://github.com/coq-community/docker-coq/wiki for supported images
           - '8.16'
           - '8.17'
+          - '8.18'
           - 'dev'
         bit_size:
           - 32
@@ -32,6 +33,8 @@ jobs:
         exclude:   
           - coq_version: 8.16
             bit_size: 32
+          - coq_version: 8.17
+            bit_size: 32
           - coq_version: dev
             bit_size: 32
     steps:
@@ -50,7 +53,7 @@ jobs:
             endGroup
           install: |
             startGroup "Install dependencies"
-              opam install -y ${{ matrix.coq_version == 'dev' && 'coq-flocq' || matrix.bit_size == 32 && 'coq-compcert-32.3.12' || 'coq-compcert.3.12' }}
+              opam install -y ${{ matrix.coq_version == 'dev' && 'coq-flocq' || matrix.bit_size == 32 && 'coq-compcert-32.3.13' || 'coq-compcert.3.13' }}
               # Required by test2
               opam install -y coq-ext-lib
             endGroup
@@ -61,7 +64,7 @@ jobs:
             endGroup
           script: |
             startGroup "Build & Install"
-              make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=${{ matrix.coq_version=='dev' && 'bundled' || 'platform' }} IGNORECOQVERSION=true
+              make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=${{ matrix.coq_version=='dev' && 'bundled' || 'platform' }} IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
             endGroup
           after_script: |
             startGroup 'Copy Opam coq/user-contrib and coq-variant'
@@ -88,6 +91,7 @@ jobs:
         coq_version:
           - '8.16'
           - '8.17'
+          - '8.18'
           - 'dev' 
         make_target:
           - assumptions.txt
@@ -102,6 +106,8 @@ jobs:
         exclude:
           - coq_version: 8.16
             bit_size: 32
+          - coq_version: 8.17
+            bit_size: 32
           - coq_version: dev
             bit_size: 32
           - bit_size: 64
@@ -134,7 +140,7 @@ jobs:
             endGroup
           script: |
             startGroup "Build & Install"
-              make -f util/make-touch  IGNORECOQVERSION=true
-              make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=${{ matrix.coq_version=='dev' && 'bundled' || 'platform' }}  IGNORECOQVERSION=true
+              make -f util/make-touch  IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
+              make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=${{ matrix.coq_version=='dev' && 'bundled' || 'platform' }}  IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
             endGroup
           uninstall:
diff --git a/CHANGES b/CHANGES
index 001a84128..7efbfc880 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,4 +1,4 @@
-CHANGES IN NEXT RELEASE (after 2.12)
+CHANGES IN RELEASE 2.13 (October 2023)
 
 - Improved error diagnostics when compspecs mismatch
 - Improved error diagnostics when change_compspecs fails
@@ -7,6 +7,10 @@ CHANGES IN NEXT RELEASE (after 2.12)
 - forward tactic is slightly more careful about not simplifying user's terms
 - bug fixes and improved diagnostic messages in list_solve tactic
 - field_compatible0_Tarray_offset no longer requires naturally_aligned hypothesis
+- 'forward' now interacts better with 'localize/unlocalize' (#773)
+- Performance improvements in VSU system (#716)
+- VSU permits sharing of globals between compilation units (#713)
+- Compatible with Coq 8.18.0, 8.17.1, 8.16.1; with CompCert 3.13.1, 3.12, 3.11.
 
 CHANGES IN RELEASE 2.12 (March 2023)
 
diff --git a/InteractionTrees b/InteractionTrees
index eede8c539..8e28e2ee0 160000
--- a/InteractionTrees
+++ b/InteractionTrees
@@ -1 +1 @@
-Subproject commit eede8c539985e358e7149ab77b5c058def37571d
+Subproject commit 8e28e2ee08496c696e03916a22d93c39559a9715
diff --git a/Makefile b/Makefile
index b9742c7a0..84412fa86 100644
--- a/Makefile
+++ b/Makefile
@@ -21,7 +21,7 @@ COQLIB=$(shell $(COQC) -where | tr -d '\r' | tr '\\' '/')
 
 # Check Coq version
 
-COQVERSION= 8.16.0 or-else 8.16.1 or-else 8.17+rc1 or-else 8.17 or-else 8.17.0 or-else 8.17.1
+COQVERSION= 8.16.0 or-else 8.16.1 or-else 8.17+rc1 or-else 8.17 or-else 8.17.0 or-else 8.17.1 or-else 8.18.0
 
 COQV=$(shell $(COQC) -v)
 ifneq ($(IGNORECOQVERSION),true)
diff --git a/VERSION b/VERSION
index 3e162f02e..ae656d473 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-2.12
+2.13
diff --git a/atomics/verif_atomics.v b/atomics/verif_atomics.v
index 3aae279d5..030a97e00 100644
--- a/atomics/verif_atomics.v
+++ b/atomics/verif_atomics.v
@@ -678,7 +678,7 @@ Lemma full_hist'_drop : forall h h' v (Hh : full_hist' h v)
   full_hist' h' v.
 Proof.
   intros ??? (l & Hl & Hv) ?.
-  revert dependent h'; revert dependent v; revert dependent h; induction l using rev_ind; intros.
+  generalize dependent h'; generalize dependent v; generalize dependent h; induction l using rev_ind; intros.
   - inv Hl; simpl in *.
     destruct h'.
     exists []; auto.
@@ -748,7 +748,7 @@ Corollary full_hist_nil' : forall n l (Hfull : Forall2 full_hist' (repeat [] n)
   (Hrep : Forall repable_signed l), l = repeat 0 n.
 Proof.
   intros; apply full_hist'_nil in Hfull.
-  revert dependent l; induction n; destruct l; auto; try discriminate; simpl; intros.
+  generalize dependent l; induction n; destruct l; auto; try discriminate; simpl; intros.
   inv Hrep; f_equal; [|apply IHn; inv Hfull; auto].
   apply repr_inj_signed; auto; congruence.
 Qed.
diff --git a/atomics/verif_hashtable1.v b/atomics/verif_hashtable1.v
index 863beebd8..f58f4095d 100644
--- a/atomics/verif_hashtable1.v
+++ b/atomics/verif_hashtable1.v
@@ -1413,7 +1413,7 @@ Proof.
   rewrite Zlength_correct in H.
   assert (length h = Z.to_nat size) as Hlen by Omega0.
   forget (Z.to_nat size) as n; clear H.
-  revert dependent h; induction n; destruct h; auto; intros; inv Hlen; simpl.
+  generalize dependent h; induction n; destruct h; auto; intros; inv Hlen; simpl.
   destruct p; rewrite IHn; auto.
 Qed.
 
@@ -1502,7 +1502,7 @@ Proof.
   rewrite Zlength_correct in H.
   assert (length h = Z.to_nat size) as Hlen by Omega0.
   forget (Z.to_nat size) as n; clear H.
-  revert dependent h; induction n; destruct h; auto; intros; inv Hlen; simpl.
+  generalize dependent h; induction n; destruct h; auto; intros; inv Hlen; simpl.
   destruct p; rewrite IHn, !app_nil_r; auto.
 Qed.
 
@@ -1950,7 +1950,7 @@ Lemma one_CAS_succeeds : forall h v a t1 t2 b1 b2 (Hl : full_hist' h v) (Hin1 :
 Proof.
   intros.
   destruct Hl as (l & Hl & Hv).
-  revert dependent v; induction Hl; [contradiction|].
+  generalize dependent v; induction Hl; [contradiction|].
   subst; intros; rewrite !in_app in *; simpl in *.
   rewrite Forall_app in Ha; destruct Ha as (? & Ha); inv Ha.
   rewrite apply_hist_app in Hv.
diff --git a/atomics/verif_ptr_atomics.v b/atomics/verif_ptr_atomics.v
index 4a9b99d55..896178c09 100644
--- a/atomics/verif_ptr_atomics.v
+++ b/atomics/verif_ptr_atomics.v
@@ -839,7 +839,7 @@ Lemma full_hist'_drop : forall h h' v (Hh : full_hist' h v)
   full_hist' h' v.
 Proof.
   intros ??? (l & Hl & Hv) ?.
-  revert dependent h'; revert dependent v; revert dependent h; induction l using rev_ind; intros.
+  generalize dependent h'; generalize dependent v; generalize dependent h; induction l using rev_ind; intros.
   - inv Hl; simpl in *.
     destruct h'.
     exists []; auto.
diff --git a/compcert/Makefile.config b/compcert/Makefile.config
index 8fb870d00..d9dc735a1 100644
--- a/compcert/Makefile.config
+++ b/compcert/Makefile.config
@@ -6,7 +6,7 @@ SHAREDIR=$(PREFIX)/share
 COQDEVDIR=$(PREFIX)/lib/compcert/coq
 OCAML_NATIVE_COMP=true
 OCAML_OPT_COMP=true
-MENHIR_DIR=/usr/local/lib/menhirLib
+MENHIR_DIR=/Users/appel/.opam/CP.2023.03.0~8.18+beta1/lib/menhirLib
 COMPFLAGS=-bin-annot
 ABI=standard
 ARCH=x86
@@ -20,7 +20,7 @@ CLIGHTGEN=true
 CLINKER=gcc
 CLINKER_OPTIONS=-m64 -no-pie
 CPREPRO=gcc
-CPREPRO_OPTIONS=-std=c99 -m64 -U__GNUC__ '-D__attribute__(x)=' -E
+CPREPRO_OPTIONS=-m64 -U__GNUC__ -U__SIZEOF_INT128__ -E
 ARCHIVER=ar rcs
 ENDIANNESS=little
 HAS_RUNTIME_LIB=true
@@ -28,7 +28,7 @@ HAS_STANDARD_HEADERS=true
 INSTALL_COQDEV=true
 LIBMATH=-lm
 MODEL=64
-SYSTEM=cygwin
+SYSTEM=linux
 RESPONSEFILE=gnu
-LIBRARY_FLOCQ=external
+LIBRARY_FLOCQ=local
 LIBRARY_MENHIRLIB=local
diff --git a/compcert/VERSION b/compcert/VERSION
index a3233349b..1d99ed706 100644
--- a/compcert/VERSION
+++ b/compcert/VERSION
@@ -1,4 +1,4 @@
-version=3.12
+version=3.13
 buildnr=
 tag=
 branch=
diff --git a/compcert/cfrontend/Cstrategy.v b/compcert/cfrontend/Cstrategy.v
index ce965672a..3c45e93b6 100644
--- a/compcert/cfrontend/Cstrategy.v
+++ b/compcert/cfrontend/Cstrategy.v
@@ -1653,8 +1653,8 @@ Definition outcome_result_value (out: outcome) (t: type) (v: val) (m: mem) : Pro
   | _, _ => False
   end.
 
-(** [eval_expression ge e m1 a t m2 a'] describes the evaluation of the
-  complex expression e.  [v] is the resulting value, [m2] the final
+(** [eval_expression ge e m1 a t m2 v] describes the evaluation of the
+  complex expression [a].  [v] is the resulting value, [m2] the final
   memory state, and [t] the trace of input/output events performed
   during this evaluation.  *)
 
diff --git a/concurrency/ghosts.v b/concurrency/ghosts.v
index c6f5c88f0..5152e2e17 100644
--- a/concurrency/ghosts.v
+++ b/concurrency/ghosts.v
@@ -1548,7 +1548,7 @@ Lemma hist_list'_add : forall h1 h2 (l : list hist_el) (Hdisj : disjoint h1 h2),
 Proof.
   intros.
   remember (map_add h1 h2) as h.
-  revert dependent h2; revert h1; induction H; intros.
+  generalize dependent h2; revert h1; induction H; intros.
   - exists [], []; split; [reflexivity|].
     assert (h1 = empty_map /\ h2 = empty_map) as [].
     { split; extensionality k; apply equal_f with (x := k) in Heqh; unfold map_add in Heqh;
diff --git a/floyd/SeparationLogicAsLogic.v b/floyd/SeparationLogicAsLogic.v
index 084f28e65..b529f82da 100644
--- a/floyd/SeparationLogicAsLogic.v
+++ b/floyd/SeparationLogicAsLogic.v
@@ -109,7 +109,7 @@ with labeled_statements_ind (L: labeled_statements): all_suf_of_labeled_statemen
 End statement_ind.
 
 Ltac induction_stmt s :=
-  revert dependent s;
+  generalize dependent s;
   let s1 := fresh s "1" in
   let s2 := fresh s "2" in
   let IHs := fresh "IH" s in
diff --git a/floyd/VSU.v b/floyd/VSU.v
index eed14d3d6..c9682d738 100644
--- a/floyd/VSU.v
+++ b/floyd/VSU.v
@@ -2190,7 +2190,7 @@ eapply Comp_Exports_sub2;
 - symmetry in NOimports |- *.
    unfold JoinedImports in *.
    change (filter _ nil) with (@nil (ident*funspec)) in *.
-   rewrite <- app_nil_end in *.
+   rewrite app_nil_r in *.
    match goal with |- filter ?A (filter ?B ?C) = _ => forget A as F; forget B as G; forget C as al end.
    clear - NOimports.
    induction al as [|[i?]]; auto.
@@ -3051,7 +3051,7 @@ assert (H20: forall i fd, In (i,fd) (prog_funct' (map of_builtin (QP.prog_builti
 }
 
 assert (VG_LNR: list_norepet (map fst (QPvarspecs p) ++ map fst  G)). {
-  pose proof (Comp_LNR c). rewrite <- app_nil_end in H4.
+  pose proof (Comp_LNR c). rewrite app_nil_r in H4.
   auto.
 }
 forget (filter isGfun (PTree.elements (QP.prog_defs p))) as fs.
diff --git a/floyd/canon.v b/floyd/canon.v
index c0e6095e0..c62eaab59 100644
--- a/floyd/canon.v
+++ b/floyd/canon.v
@@ -37,7 +37,14 @@ Fixpoint fold_right_andp rho (l: list (environ -> Prop)) : Prop :=
  end.
 
 Declare Scope assert.  Delimit Scope assert with assert.
+Global Set Warnings "-overwriting-delimiting-key".
 Delimit Scope assert with argsassert.
+(* Ideally we would like to disable this warning only for this Delimit command,
+ and then do 
+   Set Warnings "+overwriting-delimiting-key".
+  afterward, but this doesn't really work, because we'd still
+ get the warning in every file that imports this file.
+*)
 Declare Scope assert3. Delimit Scope assert3 with assert3.
 Declare Scope assert4. Delimit Scope assert4 with assert4.
 Declare Scope assert5. Delimit Scope assert5 with assert5.
@@ -311,7 +318,7 @@ Proof.
   specialize (H0 n ts x rho).
   simpl in H0.
   match goal with H : Forall2 _ _ (map _ ?l) |- _ => forget l as Q1 end.
-  revert dependent Q1; induction (Q ts x); intros; inv H0; destruct Q1; try discriminate.
+  generalize dependent Q1; induction (Q ts x); intros; inv H0; destruct Q1; try discriminate.
   + auto.
   + inv H3.
     simpl.
@@ -355,7 +362,7 @@ Proof.
   specialize (H0 n ts x rho).
   simpl in H0.
   match goal with H : Forall2 _ _ (map _ ?l) |- _ => forget l as P1 end.
-  revert dependent P1; induction (P ts x); intros; inv H0; destruct P1; try discriminate.
+  generalize dependent P1; induction (P ts x); intros; inv H0; destruct P1; try discriminate.
   + auto.
   + inv H3.
     simpl.
@@ -1085,7 +1092,7 @@ Ltac frame_SEP' L :=  (* this should be generalized to permit framing on LOCAL p
  match goal with
  | |- @semax _ _ _ (PROPx _ (LOCALx ?Q (SEPx ?R))) _ _ =>
   rewrite <- (Floyd_firstn_skipn (length L) R);
-  rewrite (app_nil_end Q);
+  rewrite (app_nil_r Q);
     simpl length; unfold Floyd_firstn, Floyd_skipn;
     eapply (semax_frame_PQR);
       [ unfold closed_wrt_modvars;  auto 50 with closed
@@ -1494,7 +1501,7 @@ inv H.
 specialize (IHn _ H). clear H.
 simpl Floyd_firstn.
 change (m :: Floyd_firstn n R) with (app (m::nil) (Floyd_firstn n R)).
-rewrite app_ass. unfold app at 1.
+rewrite <- app_assoc. unfold app at 1.
 simpl.
 f_equal.
 auto.
@@ -2710,7 +2717,7 @@ Proof.
   specialize (H0 n ts x (Clight_seplog.mkEnv (fst gargs) nil nil)).
   simpl in H0.
   match goal with H : Forall2 _ _ (map _ ?l) |- _ => forget l as Q1 end.
-  revert dependent Q1; induction (G ts x); intros; inv H0; destruct Q1; try discriminate.
+  generalize dependent Q1; induction (G ts x); intros; inv H0; destruct Q1; try discriminate.
   + auto.
   + inv H3.
     simpl.
@@ -2756,7 +2763,7 @@ Proof.
   specialize (H0 n ts x any_environ).
   simpl in H0.
   match goal with H : Forall2 _ _ (map _ ?l) |- _ => forget l as P1 end.
-  revert dependent P1; induction (P ts x); intros; inv H0; destruct P1; try discriminate.
+  generalize dependent P1; induction (P ts x); intros; inv H0; destruct P1; try discriminate.
   + auto.
   + inv H3.
     simpl.
diff --git a/floyd/field_at.v b/floyd/field_at.v
index a77d72c53..e4ef2939d 100644
--- a/floyd/field_at.v
+++ b/floyd/field_at.v
@@ -2758,7 +2758,7 @@ Proof.
   setoid_rewrite aggregate_pred.rangespec_ext at 4; [|intros; rewrite Z.sub_0_r; apply f_equal; auto].
   clear H3 H4.
   rewrite Z2Nat_max0 in *.
-  forget (offset_val 0 p) as p'; forget (Z.to_nat z) as n; forget 0 as lo; revert dependent lo; induction n; auto; simpl; intros.
+  forget (offset_val 0 p) as p'; forget (Z.to_nat z) as n; forget 0 as lo; generalize dependent lo; induction n; auto; simpl; intros.
  apply derives_refl.
   match goal with |- (?P1 * ?Q1) * (?P2 * ?Q2) |-- _ =>
     eapply derives_trans with (Q := (P1 * P2) * (Q1 * Q2)); [cancel|] end.
@@ -2825,8 +2825,7 @@ Qed.
 #[export] Hint Rewrite
   @field_at_data_at_cancel'
   @field_at_data_at
-  @field_at__data_at_
-  @data_at__data_at : cancel.
+  @field_at__data_at_ : cancel.
 
 (* END new experiments *)
 
diff --git a/floyd/forward.v b/floyd/forward.v
index 58cc8577b..e396a237b 100644
--- a/floyd/forward.v
+++ b/floyd/forward.v
@@ -1173,19 +1173,40 @@ Ltac simplify_remove_localdef_temp :=
     change u with u'
   end.
 
+Ltac afc_error1 :=
+  fail 100 "Error: should not hit this case in after_forward_call.  To ignore this error and try anyway, do 'Ltac afc_error1 ::= idtac'".
+
 Ltac after_forward_call :=
     check_POSTCONDITION; 
     try match goal with |- context [remove_localdef_temp] =>
               simplify_remove_localdef_temp
      end;
-    unfold_app; 
     try (apply extract_exists_pre; intros _); 
     match goal with
         | |- semax _ _ _ _ => idtac
         | |- unit -> semax _ _ _ _ => intros _
     end;
     match goal with
-        | |- @semax ?CS _ _ _ _ _ => try change_compspecs CS
+        | |- @semax ?CS ?Espec ?Delta (exp ?F) ?c ?Post =>
+               lazymatch F with context [@app mpred _ ?x] =>
+                  let hide := fresh "hide" in set (hide := x);
+                  try change_compspecs CS;
+                  subst hide
+               end;
+               unfold_app
+        | |- @semax ?CS ?Espec ?Delta (PROPx (?P1 ++ ?P2) (LOCALx ?Q (SEPx (?A ++ ?B)))) ?c ?Post =>
+               let hide := fresh "hide" in
+               pose (hide x := @semax CS Espec Delta (PROPx (P1 ++ P2) 
+                                     (LOCALx Q (SEPx (x ++ B)))) c Post);
+               change (hide A);
+               try change_compspecs CS;
+               subst hide; 
+               cbv beta;
+               unfold_app
+        | |- @semax ?CS _ _ _ _ _ => 
+               afc_error1;
+               unfold_app;
+               try change_compspecs CS
     end;
     repeat (apply semax_extract_PROP; intro); 
     cleanup_no_post_exists; 
@@ -1346,7 +1367,10 @@ Ltac prove_call_setup_aux  ts witness :=
  | check_vl_eq_args
  | auto 50 with derives
  | check_gvars_spec
- | try change_compspecs CS; cancel_for_forward_call
+ | let lhs := fresh "lhs" in 
+   match goal with |- ?A |-- ?B => pose (lhs := A); change (lhs |-- B) end;
+   try change_compspecs CS; subst lhs;
+   cancel_for_forward_call
  |
  ])
   in strip1_later R' cR
diff --git a/floyd/freezer.v b/floyd/freezer.v
index 15152e48a..f4f41e932 100644
--- a/floyd/freezer.v
+++ b/floyd/freezer.v
@@ -576,7 +576,7 @@ induction n; destruct R; intros.
 + inv H.
   specialize (IHn _ H1). clear H1. simpl Floyd_firstn.
   change (m :: Floyd_firstn n R) with (app (m::nil) (Floyd_firstn n R)).
-  rewrite app_ass. unfold app at 1.
+  rewrite <- app_assoc. unfold app at 1.
   simpl; f_equal; auto.
 Qed.
 
diff --git a/floyd/globals_lemmas.v b/floyd/globals_lemmas.v
index fd64a7850..8a6c302f8 100644
--- a/floyd/globals_lemmas.v
+++ b/floyd/globals_lemmas.v
@@ -111,7 +111,7 @@ Proof. induction xs; intros; simpl.
    apply sepcon_derives.
    + rewrite (data_at_singleton_array_eq Ews tint (Vint a)) by trivial.
      erewrite mapsto_data_at'; auto; trivial.
-     red; simpl; intuition.
+     red; simpl; intuition auto with *.
      econstructor. reflexivity. simpl; trivial.
    + eapply derives_trans. apply IHxs; clear IHxs.
      * rewrite ! Ptrofs.unsigned_repr; try rep_lia.
@@ -121,7 +121,7 @@ Proof. induction xs; intros; simpl.
        replace (Z.succ (Zlength xs) - 1) with (Zlength xs) by lia.
        apply derives_refl'. f_equal. list_solve.
        unfold field_address0. rewrite if_true; simpl; trivial.
-       red; intuition.
+       red; intuition auto with *.
        -- reflexivity.
        -- red. rewrite sizeof_Tarray, Z.max_r. simpl sizeof; rep_lia. list_solve.
        -- eapply align_compatible_rec_Tarray; intros.
diff --git a/floyd/local2ptree_denote.v b/floyd/local2ptree_denote.v
index 238a4d61b..622386f69 100644
--- a/floyd/local2ptree_denote.v
+++ b/floyd/local2ptree_denote.v
@@ -223,7 +223,7 @@ Proof.
       apply PTree.elements_complete in H0.
       destruct H; try subst q; eauto 50.
       specialize (IHL H (K ++ (i, (t, v)) :: nil));
-      rewrite app_ass in IHL; specialize (IHL HeqL); eauto.
+      rewrite <- app_assoc in IHL; specialize (IHL HeqL); eauto.
   + destruct H.
     - subst q.
       assert (In a (PTree.elements T1)).
@@ -231,7 +231,7 @@ Proof.
       destruct a as [i v]; apply PTree.elements_complete in H; eauto.
     - destruct a as [i v].
       specialize (IHL H (K ++ (i,v)::nil)).
-      rewrite app_ass in IHL; specialize (IHL HeqL); eauto.
+      rewrite <- app_assoc in IHL; specialize (IHL HeqL); eauto.
 Qed.
 
 Lemma in_temp_aux:
@@ -704,7 +704,7 @@ Lemma local2ptree_soundness  : forall P Q R T1 T2 P' Q',
   PROPx P (LOCALx Q (SEPx R)) = PROPx (P' ++ P) (LOCALx (LocalD T1 T2 Q') (SEPx R)).
 Proof. intros. eapply local2ptree_soundness' in H.
    etransitivity; [ | apply H]. clear H.
-   simpl. rewrite <- app_nil_end; auto.
+   simpl. rewrite app_nil_r; auto.
 Qed.
 
 Lemma local2ptree_soundness'' : forall Q T1 T2 gv,
diff --git a/mailbox/verif_mailbox_bad_write.v b/mailbox/verif_mailbox_bad_write.v
index f24befbba..fa8335af4 100644
--- a/mailbox/verif_mailbox_bad_write.v
+++ b/mailbox/verif_mailbox_bad_write.v
@@ -1095,7 +1095,7 @@ Proof.
         rewrite In_upto, Z2Nat.id in *; unfold N; try lia.
         apply Forall_Znth; [lia | auto].
       * assert (Zlength h' = Zlength h) as Hlen by lia; assert (Zlength t' = Zlength h') as Hlen' by lia;
-        clear - Hlen Hlen'; revert dependent h; revert dependent t'; induction h';
+        clear - Hlen Hlen'; generalize dependent h; generalize dependent t'; induction h';
           destruct h, t'; rewrite ?Zlength_nil, ?Zlength_cons in *; simpl; intros; auto;
           try (rewrite Zlength_correct in *; lia).
         constructor; eauto.
diff --git a/mailbox/verif_mailbox_write.v b/mailbox/verif_mailbox_write.v
index fa837cb64..50a5a2ebb 100644
--- a/mailbox/verif_mailbox_write.v
+++ b/mailbox/verif_mailbox_write.v
@@ -1020,7 +1020,7 @@ Proof.
         rewrite In_upto, Z2Nat.id in *; unfold N; try lia.
         apply Forall_Znth; [lia | auto].
       * assert (Zlength h' = Zlength h) as Hlen by lia; assert (Zlength t' = Zlength h') as Hlen' by lia;
-        clear - Hlen Hlen'; revert dependent h; revert dependent t'; induction h';
+        clear - Hlen Hlen'; generalize dependent h; generalize dependent t'; induction h';
           destruct h, t'; rewrite ?Zlength_nil, ?Zlength_cons in *; simpl; intros; auto;
           try (rewrite Zlength_correct in *; lia).
         constructor; eauto.
diff --git a/msl/age_sepalg.v b/msl/age_sepalg.v
index ca4709ea0..b56cfca0e 100644
--- a/msl/age_sepalg.v
+++ b/msl/age_sepalg.v
@@ -540,7 +540,7 @@ Qed.
 Lemma unlaterR_core {A}{JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{agA: ageable A}{AgeA: Age_alg A}:
   forall x y : A, laterR (core x) y -> exists y0, laterR x y0 /\ y = core y0.
 Proof.
-  intros; remember (core x) as cx; revert dependent x; induction H; intros; subst.
+  intros; remember (core x) as cx; generalize dependent x; induction H; intros; subst.
   - pose proof (age_level _ _ H) as Hlevel.
     rewrite level_core in Hlevel.
     destruct (levelS_age1 _ _ Hlevel) as (y0 & Hage).
diff --git a/msl/corable.v b/msl/corable.v
index 2bde32bc7..201c2f890 100644
--- a/msl/corable.v
+++ b/msl/corable.v
@@ -74,7 +74,7 @@ Qed.
 Lemma ext_later_compat {A}{agA: ageable A}{EO: Ext_ord A}: forall a b a', ext_order a b -> laterR a a' -> exists b', laterR b b' /\ ext_order a' b'.
 Proof.
   intros.
-  revert dependent b; induction H0; intros.
+  generalize dependent b; induction H0; intros.
   - eapply ext_age_compat in H as (? & ? & ?); eauto.
     do 2 eexists; [|eauto].
     apply t_step; auto.
diff --git a/msl/predicates_hered.v b/msl/predicates_hered.v
index 8b8023dd4..83ed845cc 100644
--- a/msl/predicates_hered.v
+++ b/msl/predicates_hered.v
@@ -130,7 +130,7 @@ Qed.
 (*Lemma ext_later_commut : commut A ext_order laterR.
 Proof.
   repeat intro.
-  revert dependent x; induction H0; intros.
+  generalize dependent x; induction H0; intros.
   - eapply ext_age_commut in H as []; eauto.
     eexists; [|apply H1].
     apply t_step; auto.
@@ -152,7 +152,7 @@ Qed.*)
 Lemma later_ext_commut : commut A laterR ext_order.
 Proof.
   repeat intro.
-  revert dependent z; induction H; intros.
+  generalize dependent z; induction H; intros.
   - eapply age_ext_commut in H as []; eauto.
     eexists; [apply H|].
     apply t_step; auto.
@@ -286,7 +286,7 @@ Qed.
 Lemma valid_rel_later : valid_rel laterR.
 Proof.
   intros; split; hnf; intros.
-  revert dependent x.
+  generalize dependent x.
   induction H0; intros.
   exists y; auto.
   apply t_step; auto.
@@ -309,7 +309,7 @@ Qed.
 Lemma valid_rel_nec : valid_rel necR.
 Proof.
   intros; split; hnf; intros.
-  revert dependent x.
+  generalize dependent x.
   induction H0; intros.
   exists y; auto.
   apply rt_step; auto.
diff --git a/progs/VSUpile/verif_stdlib.v b/progs/VSUpile/verif_stdlib.v
index b92f3b460..0469bed9e 100644
--- a/progs/VSUpile/verif_stdlib.v
+++ b/progs/VSUpile/verif_stdlib.v
@@ -6,10 +6,16 @@ Require Import spec_stdlib.
 
 Require VST.veric.version. From Coq Require Import String.
 Lemma version_test: False.
- assert (VST.veric.version.compcert_version = stdlib.Info.version \/
-         VST.veric.version.compcert_version = "3.12"%string /\
-	  stdlib.Info.version = "3.11"%string) by (compute; auto).
- assert (VST.veric.version.bitsize = stdlib.Info.bitsize) by reflexivity.
+ assert ((VST.veric.version.compcert_version = "3.11"%string \/
+          VST.veric.version.compcert_version = "3.12"%string \/ 
+          VST.veric.version.compcert_version = "3.13"%string) /\
+         (stdlib.Info.version = "3.11"%string \/
+          stdlib.Info.version = "3.12"%string \/
+          stdlib.Info.version = "3.13"%string))
+       by (compute; auto;
+            match goal with |- ?G => fail 100 "Version mismatch; cannot prove" G end).
+ assert (VST.veric.version.bitsize = stdlib.Info.bitsize) by
+    (try reflexivity; match goal with |- ?G => fail 100 "Bitsize mismatch; cannot prove" G end).
 Abort.
 
 #[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
diff --git a/progs/conc_queue_specs.v b/progs/conc_queue_specs.v
index dd4cfcd1d..495ad255c 100644
--- a/progs/conc_queue_specs.v
+++ b/progs/conc_queue_specs.v
@@ -241,7 +241,7 @@ Qed.
 Lemma interleave_single : forall {A} (l l' : list A), interleave [l] l' = (l' = l).
 Proof.
   intros; apply prop_ext; split; intro; subst.
-  - remember [l] as l0; revert dependent l; induction H; intros; subst.
+  - remember [l] as l0; generalize dependent l; induction H; intros; subst.
     + inv Hnil; auto.
     + exploit (Znth_inbounds i [l0] []).
       { rewrite Hcons; discriminate. }
@@ -257,7 +257,7 @@ Lemma interleave_remove_nil : forall {A} ls (l' : list A),
   interleave ([] :: ls) l' <-> interleave ls l'.
 Proof.
   split; intro.
-  - remember ([] :: ls) as l0; revert dependent ls; induction H; intros; subst.
+  - remember ([] :: ls) as l0; generalize dependent ls; induction H; intros; subst.
     + inv Hnil; constructor; auto.
     + destruct (Z_le_dec i 0).
       { destruct (eq_dec i 0); [subst; rewrite Znth_0_cons in Hcons | rewrite Znth_underflow in Hcons];
@@ -289,7 +289,7 @@ Lemma interleave_trans : forall {A} ls1 ls2 (l' l'' : list A)
 Proof.
   intros until 1; revert ls2 l''; induction Hl'; intros.
   - rewrite interleave_remove_nil in Hl''; rewrite interleave_remove_nils; auto.
-  - remember ((a :: l') :: ls2) as ls0; revert dependent ls2; revert dependent l'; revert dependent a;
+  - remember ((a :: l') :: ls2) as ls0; generalize dependent ls2; generalize dependent l'; generalize dependent a;
       induction Hl''; intros; subst.
     { inv Hnil; discriminate. }
     exploit (Znth_inbounds i ls []).
@@ -669,7 +669,7 @@ Lemma interleave_reorder : forall {A} ls1 ls2 (l l' : list A),
   interleave (ls1 ++ l :: ls2) l' <-> interleave (l :: ls1 ++ ls2) l'.
 Proof.
   split; intro.
-  - remember (ls1 ++ l :: ls2) as l0; revert dependent ls2; revert l ls1; induction H; intros; subst.
+  - remember (ls1 ++ l :: ls2) as l0; generalize dependent ls2; revert l ls1; induction H; intros; subst.
     + constructor; rewrite Forall_app in Hnil.
       destruct Hnil as (? & Hnil); inv Hnil; constructor; auto; rewrite Forall_app; auto.
     + exploit (Znth_inbounds i (ls1 ++ l0 :: ls2) []); [rewrite Hcons; discriminate | intro].
@@ -694,7 +694,7 @@ Proof.
         apply IHinterleave.
         rewrite upd_Znth_app2, upd_Znth_cons; rewrite ?Zlength_cons; try lia.
         replace (i - Zlength ls1 - 1) with (i - 1 - Zlength ls1); Omega0.
-  - remember (l :: ls1 ++ ls2) as l0; revert dependent ls2; revert l ls1; induction H; intros; subst.
+  - remember (l :: ls1 ++ ls2) as l0; generalize dependent ls2; revert l ls1; induction H; intros; subst.
     + inv Hnil; constructor.
       rewrite Forall_app in H2; destruct H2; rewrite Forall_app; split; auto.
     + exploit (Znth_inbounds i (l0 :: ls1 ++ ls2) []); [rewrite Hcons; discriminate | intro].
@@ -742,7 +742,7 @@ Lemma interleave_map_inj : forall {A B} (f : A -> B) ls l' (Hinj : forall x y, f
   interleave (map (map f) ls) (map f l') -> interleave ls l'.
 Proof.
   intros.
-  remember (map (map f) ls) as ls0; remember (map f l') as l1; revert dependent l'; revert dependent ls;
+  remember (map (map f) ls) as ls0; remember (map f l') as l1; generalize dependent l'; generalize dependent ls;
     induction H; intros; subst.
   - destruct l'; [|discriminate].
     constructor.
@@ -767,7 +767,7 @@ Lemma interleave_combine : forall {A B} ls1 ls2 (l1 : list A) (l2 : list B)
 Proof.
   intros.
   remember (map (fun x => let '(la, lb) := x in combine la lb) (combine ls1 ls2)) as ls0;
-    remember (combine l1 l2) as l0; revert dependent l2; revert l1; revert dependent ls2; revert ls1;
+    remember (combine l1 l2) as l0; generalize dependent l2; revert l1; generalize dependent ls2; revert ls1;
     induction H; intros; subst.
   - destruct l1, l2; try discriminate.
     pose proof (mem_lemmas.Forall2_Zlength Hls).
diff --git a/progs/dry_mem_lemmas.v b/progs/dry_mem_lemmas.v
index 6c35ff926..5ec757400 100644
--- a/progs/dry_mem_lemmas.v
+++ b/progs/dry_mem_lemmas.v
@@ -370,7 +370,7 @@ Proof.
   { rewrite Z.max_r in Hlim by rep_lia; lia. }
   clear Heqlo Hlen.
   clear dependent z.
-  revert dependent phi; revert dependent lo.
+  generalize dependent phi; generalize dependent lo.
   induction n; intros; subst.
   - unfold sublist; simpl.
     rewrite skipn_firstn,  Z.add_0_l, Nat.sub_diag.
@@ -785,7 +785,7 @@ Proof.
   assert (lo + Z.of_nat n = Zlength lv) as Hlen.
   { subst; rewrite Z2Nat.id; rep_lia. }
   clear Heqlo Heqn.
-  revert dependent lo; revert dependent phi; induction n; intros.
+  generalize dependent lo; generalize dependent phi; induction n; intros.
   - rewrite res_predicates.VALspec_range_0 in Hdata; simpl.
     apply inflate_emp; auto.
   - rewrite Nat2Z.inj_succ, res_predicates.VALspec_range_split2 with (n := 1)(m := Z.of_nat n) in Hdata by lia.
diff --git a/progs/verif_append.v b/progs/verif_append.v
index 7ed348424..5fe883bc5 100644
--- a/progs/verif_append.v
+++ b/progs/verif_append.v
@@ -76,7 +76,7 @@ forward_if.
    forward.
    subst s1b. subst s1.
   Exists (s1a++[a],s4,u,u2,a1).  simpl fst; simpl snd. entailer!.
-  rewrite app_ass. reflexivity.
+  rewrite <- app_assoc. reflexivity.
  +
     clear a s3 H0. subst u0. rewrite lseg_eq by reflexivity. Intros. subst s1 s1b.
     forward.
diff --git a/progs/verif_append2.v b/progs/verif_append2.v
index 45c662943..f696ea219 100644
--- a/progs/verif_append2.v
+++ b/progs/verif_append2.v
@@ -186,20 +186,20 @@ forward_if.
    forward.
    forward.
    Exists (s1a++[a],v,s1b,u0,z). unfold fst, snd.
-   rewrite !app_ass. simpl app.
+   rewrite <- !app_assoc. simpl app.
    entailer!!.
    unfold lseg.
    rewrite sepcon_comm.
    clear.
    apply RAMIF_Q.trans'' with (cons a).
-   extensionality cts; simpl; rewrite app_ass; reflexivity.
+   extensionality cts; simpl; rewrite <- app_assoc; reflexivity.
    apply allp_right; intro. apply wand_sepcon_adjoint.
    unfold listrep at 2; fold listrep; Exists u0.  apply derives_refl.
  + (* after the loop *)
    forward. forward.
    Exists x. entailer!!.
    destruct H3 as [? _]. specialize (H3 (eq_refl _)). subst s1b.
-   unfold listrep at 1.  Intros. autorewrite with norm.  rewrite H0. rewrite app_ass. simpl app.
+   unfold listrep at 1.  Intros. autorewrite with norm.  rewrite H0. rewrite <- app_assoc. simpl app.
    unfold lseg.
    rewrite sepcon_assoc.
    eapply derives_trans; [apply allp_sepcon1 | ]. apply allp_left with (a::s2).
@@ -393,7 +393,7 @@ forward_if.
     forward.
     forward.
     Exists (s1a++a::nil, v0, s1b,u0,z). unfold fst, snd.
-    simpl app; rewrite app_ass.
+    simpl app; rewrite <- app_assoc.
     entailer.
     sep_apply (lseg_cons' sh a u0 t v0 z); auto.
     sep_apply (lseg_app' sh s1a [a] v0 x t u0 z); auto.
@@ -407,7 +407,7 @@ forward_if.
     entailer!!.
     sep_apply (lseg_cons sh a y t s2); auto.
     sep_apply (lseg_app_null sh [a] s2 t y); auto.
-    rewrite app_ass.
+    rewrite <- app_assoc.
     sep_apply (lseg_app_null sh s1a ([a]++s2) x t); auto.
 Qed.
 
diff --git a/progs/verif_incrN.v b/progs/verif_incrN.v
index e73a7c7fa..a6bb7a720 100644
--- a/progs/verif_incrN.v
+++ b/progs/verif_incrN.v
@@ -169,7 +169,7 @@ Proof.
   { go_lower; clear.
     rewrite !iter_sepcon2_spec.
     Intros l1 l2; subst.
-    revert dependent l2; induction l1; destruct l2; simpl; inversion 1.
+    generalize dependent l2; induction l1; destruct l2; simpl; inversion 1.
     - Exists (@nil (gname * Z)); simpl; entailer!.
     - sep_apply (IHl1 l2); auto.
       Intros l.
diff --git a/progs/verif_insertion_sort.v b/progs/verif_insertion_sort.v
index 76a4f1e03..c160d1a64 100644
--- a/progs/verif_insertion_sort.v
+++ b/progs/verif_insertion_sort.v
@@ -319,7 +319,7 @@ entailer.
 apply (exp_right p0).
 entailer!.
 destruct unsorted_list; inv H0.
-rewrite <- app_nil_end. auto.
+rewrite app_nil_r. auto.
 
 (*invariant across body *)
 focus_SEP 1.
@@ -366,7 +366,7 @@ entailer.
 apply (exp_right (sorted_list ++ [insert_val],
                            unsorted_list, sorted, next)).
 entailer!.
-rewrite app_ass; reflexivity.
+rewrite <- app_assoc; reflexivity.
 
 Lemma insert_reorder : forall v1 v2 l,
 insert v1 (insert v2 (l)) = insert v2 (insert v1 l).
diff --git a/progs/verif_merge.v b/progs/verif_merge.v
index 8a415167e..21525aed3 100644
--- a/progs/verif_merge.v
+++ b/progs/verif_merge.v
@@ -382,7 +382,7 @@ forward.
 Exists (va::a') b' (merged ++ [vb]) a_ b_' b_ begin.
 destruct (merged ++ [vb]) eqn:?. destruct merged; inv Heql.
 forget (i::l) as merged''; clear i l; subst merged''.
-rewrite app_ass.
+rewrite <- app_assoc.
 Time entailer!. (* 22 sec -> 17.33 sec *)
 rewrite butlast_snoc. rewrite last_snoc.
 rewrite @lseg_cons_eq.
@@ -486,7 +486,7 @@ remember (hmerge :: tmerge) as merged.
     destruct a; [ apply prop_right; reflexivity | ].
     simpl map; rewrite lseg_unfold.
     subst a_; entailer!.
-    elim H6; clear; intuition.
+    elim H6; clear; intuition auto with *.
   }
  subst a.
 
@@ -556,6 +556,6 @@ remember (hmerge :: tmerge) as merged.
  apply list_append_null.
  clear -Hm.
  change (butlast merged ++ ([last merged] ++ merge a b) = merged ++ merge a b).
- rewrite <-app_ass.
+ rewrite app_assoc.
  now rewrite <-snoc; auto.
 Time Qed. (* 199 sec -> 331 sec *)
diff --git a/progs/verif_reverse.v b/progs/verif_reverse.v
index fac9b0e15..6295c688e 100644
--- a/progs/verif_reverse.v
+++ b/progs/verif_reverse.v
@@ -153,7 +153,7 @@ entailer.
 apply andp_right.
 apply prop_right.
 split.
-rewrite app_ass; reflexivity.
+rewrite <- app_assoc; reflexivity.
  f_equal. rewrite sum_int_app. f_equal. simpl. apply Int.add_zero.
 rewrite map_app. simpl map.
 eapply derives_trans; [ | apply (lseg_cons_right_list LS) with (y:=t); auto].
@@ -161,7 +161,7 @@ rewrite list_cell_eq by auto.
 cancel.
 * (* After the loop *)
 forward.  (* return s; *)
-destruct cts2; [| inversion H]. rewrite <- app_nil_end.
+destruct cts2; [| inversion H]. rewrite app_nil_r.
 entailer!.
 Qed.
 
@@ -198,7 +198,7 @@ forward.  (* v = t; *)
 Exists (h::cts1,r,v,y).
  simpl fst. simpl snd. simpl rev.
 entailer!.  (* smt_test verif_reverse_example2 *)
- - rewrite app_ass. auto.
+ - rewrite <- app_assoc. auto.
  - rewrite (lseg_unroll _ sh (h::cts1)).
     apply orp_right2.
    unfold lseg_cons.
@@ -210,7 +210,7 @@ entailer!.  (* smt_test verif_reverse_example2 *)
 * (* after the loop *)
 forward.  (* return w; *)
 Exists w; entailer!.
-rewrite <- app_nil_end, rev_involutive.
+rewrite app_nil_r, rev_involutive.
 auto.
 Qed.
 
diff --git a/progs/verif_reverse2.v b/progs/verif_reverse2.v
index f414831dd..70e5f0008 100644
--- a/progs/verif_reverse2.v
+++ b/progs/verif_reverse2.v
@@ -142,7 +142,7 @@ destruct s2 as [ | h r].
    entailer!.
    Exists (h::s1,r,v,y).
    entailer!.
-   + simpl. rewrite app_ass. auto.
+   + simpl. rewrite <- app_assoc. auto.
    + unfold listrep at 3; fold listrep.
      Exists w. entailer!.
 * (* after the loop *)
@@ -151,7 +151,7 @@ Exists w; entailer!.
 rewrite (proj1 H1) by auto.
 unfold listrep at 2; fold listrep.
 entailer!.
-rewrite <- app_nil_end, rev_involutive.
+rewrite app_nil_r, rev_involutive.
 auto.
 Qed.
 
diff --git a/progs64/dry_mem_lemmas.v b/progs64/dry_mem_lemmas.v
index 6c35ff926..5ec757400 100644
--- a/progs64/dry_mem_lemmas.v
+++ b/progs64/dry_mem_lemmas.v
@@ -370,7 +370,7 @@ Proof.
   { rewrite Z.max_r in Hlim by rep_lia; lia. }
   clear Heqlo Hlen.
   clear dependent z.
-  revert dependent phi; revert dependent lo.
+  generalize dependent phi; generalize dependent lo.
   induction n; intros; subst.
   - unfold sublist; simpl.
     rewrite skipn_firstn,  Z.add_0_l, Nat.sub_diag.
@@ -785,7 +785,7 @@ Proof.
   assert (lo + Z.of_nat n = Zlength lv) as Hlen.
   { subst; rewrite Z2Nat.id; rep_lia. }
   clear Heqlo Heqn.
-  revert dependent lo; revert dependent phi; induction n; intros.
+  generalize dependent lo; generalize dependent phi; induction n; intros.
   - rewrite res_predicates.VALspec_range_0 in Hdata; simpl.
     apply inflate_emp; auto.
   - rewrite Nat2Z.inj_succ, res_predicates.VALspec_range_split2 with (n := 1)(m := Z.of_nat n) in Hdata by lia.
diff --git a/progs64/verif_append2.v b/progs64/verif_append2.v
index 48c931064..c944f4acc 100644
--- a/progs64/verif_append2.v
+++ b/progs64/verif_append2.v
@@ -187,20 +187,20 @@ forward_if.
    forward.
    forward.
    Exists (s1a++[a],v,s1b,u0,z). unfold fst, snd.
-   rewrite !app_ass. simpl app.
+   rewrite <- !app_assoc. simpl app.
    entailer!!.
    unfold lseg.
    rewrite sepcon_comm.
    clear.
    apply RAMIF_Q.trans'' with (cons a).
-   extensionality cts; simpl; rewrite app_ass; reflexivity.
+   extensionality cts; simpl; rewrite <- app_assoc; reflexivity.
    apply allp_right; intro. apply wand_sepcon_adjoint.
    unfold listrep at 2; fold listrep; Exists u0.  apply derives_refl.
  + (* after the loop *)
    forward. forward.
    Exists x. entailer!!.
    destruct H3 as [? _]. specialize (H3 (eq_refl _)). subst s1b.
-   unfold listrep at 1.  Intros. autorewrite with norm.  rewrite H0. rewrite app_ass. simpl app.
+   unfold listrep at 1.  Intros. autorewrite with norm.  rewrite H0. rewrite <- app_assoc. simpl app.
    unfold lseg.
    rewrite sepcon_assoc.
    eapply derives_trans; [apply allp_sepcon1 | ]. apply allp_left with (a::s2).
@@ -394,7 +394,7 @@ forward_if.
     forward.
     forward.
     Exists (s1a++a::nil, v0, s1b,u0,z). unfold fst, snd.
-    simpl app; rewrite app_ass.
+    simpl app; rewrite <- app_assoc.
     entailer.
     sep_apply (lseg_cons' sh a u0 t v0 z); auto.
     sep_apply (lseg_app' sh s1a [a] v0 x t u0 z); auto.
@@ -408,7 +408,7 @@ forward_if.
     entailer!!.
     sep_apply (lseg_cons sh a y t s2); auto.
     sep_apply (lseg_app_null sh [a] s2 t y); auto.
-    rewrite app_ass.
+    rewrite <- app_assoc.
     sep_apply (lseg_app_null sh s1a ([a]++s2) x t); auto.
 Qed.
 
diff --git a/progs64/verif_incrN.v b/progs64/verif_incrN.v
index 10f94b058..ca63cb6b7 100644
--- a/progs64/verif_incrN.v
+++ b/progs64/verif_incrN.v
@@ -179,7 +179,7 @@ Proof.
   { go_lower; clear.
     rewrite !iter_sepcon2_spec.
     Intros l1 l2; subst.
-    revert dependent l2; induction l1; destruct l2; simpl; inversion 1.
+    generalize dependent l2; induction l1; destruct l2; simpl; inversion 1.
     - Exists (@nil (gname * Z)); simpl; entailer!.
     - sep_apply (IHl1 l2); auto.
       Intros l.
diff --git a/progs64/verif_reverse2.v b/progs64/verif_reverse2.v
index cba8a0fed..bdc55f850 100644
--- a/progs64/verif_reverse2.v
+++ b/progs64/verif_reverse2.v
@@ -143,7 +143,7 @@ destruct s2 as [ | h r].
    entailer!.
    Exists (h::s1,r,v,y).
    entailer!.
-   + simpl. rewrite app_ass. auto.
+   + simpl. rewrite <- app_assoc. auto.
    + unfold listrep at 3; fold listrep.
      Exists w. entailer!.
 * (* after the loop *)
@@ -152,7 +152,7 @@ Exists w; entailer!.
 rewrite (proj1 H1) by auto.
 unfold listrep at 2; fold listrep.
 entailer!.
-rewrite <- app_nil_end, rev_involutive.
+rewrite app_nil_r, rev_involutive.
 auto.
 Qed.
 
diff --git a/sha/ShaInstantiation.v b/sha/ShaInstantiation.v
index 1ec14c0fe..d84bc9ba4 100644
--- a/sha/ShaInstantiation.v
+++ b/sha/ShaInstantiation.v
@@ -44,7 +44,7 @@ Lemma fpad_inner_length l (L:length l = p): (length (fpad_inner (bitsToBytes l))
 Proof.
   unfold fpad_inner. repeat rewrite app_length.
   rewrite repeat_length, length_intlist_to_bytelist.
-  rewrite (mult_comm 4), plus_comm, Zlength_correct.
+  rewrite (Nat.mul_comm 4), Nat.add_comm, Zlength_correct.
   rewrite bitsToBytes_len_gen with (n:=32%nat).
     reflexivity.
     apply L.
@@ -136,7 +136,7 @@ Proof. unfold pad_inc.
    destruct H. rewrite H. clear H.
    assert (Z.to_nat (zz mod 64 - 1) = minus (Z.to_nat (zz mod 64)) 1).
      clear - n H0. remember (zz mod 64).  clear Heqz. rewrite Z2Nat.inj_sub. reflexivity. lia.
-   rewrite H; clear H. rewrite <- NPeano.Nat.add_sub_swap. rewrite minus_Sn_m. simpl. exists k. lia.
+   rewrite H; clear H. rewrite <- NPeano.Nat.add_sub_swap. rewrite <- Nat.sub_succ_l. simpl. exists k. lia.
    lia. apply (Z2Nat.inj_le 1). lia. lia. lia.
 Qed.
 
@@ -283,13 +283,13 @@ Qed.
 
 Lemma pad_inc_injective: forall l1 l2, pad_inc l1 = pad_inc l2 -> l1=l2.
 Proof. intros.
-remember (beq_nat (length l1) (length l2)) as d.
+remember (Nat.eqb (length l1) (length l2)) as d.
 destruct d.
-{ apply beq_nat_eq in Heqd.
+{ symmetry in Heqd; rewrite Nat.eqb_eq in Heqd.
   unfold pad_inc in H. repeat rewrite Zlength_correct in H.
   rewrite <- Heqd in H.
   eapply app_inv_tail. apply H. }
-{ symmetry in Heqd; apply beq_nat_false in Heqd.
+{ symmetry in Heqd. rewrite Nat.eqb_neq in Heqd.
   unfold pad_inc in H.
   repeat rewrite app_assoc in H.
   destruct (app_inv_length2 _ _ _ _ H); clear H. reflexivity.
diff --git a/sha/call_memcpy.v b/sha/call_memcpy.v
index 76520929b..6288f73c8 100644
--- a/sha/call_memcpy.v
+++ b/sha/call_memcpy.v
@@ -63,14 +63,14 @@ pose proof (Zlength_nonneg src).
 rewrite H0.
 rewrite Z.sub_diag.
 change (Z.to_nat 0) with 0%nat; simpl.
-rewrite <- app_nil_end.
+rewrite app_nil_r.
 rewrite sublist_same by lia.
 f_equal.
-rewrite (sublist_nil hi), <- app_nil_end.
+rewrite (sublist_nil hi), app_nil_r.
 rewrite sublist_app by (rewrite ?Zlength_repeat, ?Z.max_r; lia).
 rewrite ?Z.min_l by lia.
 rewrite ?Z.max_r by lia.
-rewrite sublist_nil, <- app_nil_end.
+rewrite sublist_nil, app_nil_r.
 apply sublist_same; lia.
 Qed.
 
@@ -87,14 +87,14 @@ pose proof (Zlength_nonneg src).
 repeat rewrite Z.sub_diag.
 change (Z.to_nat 0) with 0.
 unfold repeat at 1.
-rewrite <- app_nil_end.
+rewrite app_nil_r.
 rewrite sublist_same by lia.
 f_equal.
-rewrite sublist_nil, <- app_nil_end by lia.
+rewrite sublist_nil, app_nil_r by lia.
 rewrite sublist_app by (rewrite ?Zlength_repeat, ?Z.max_r; lia).
 rewrite ?Z.min_l by lia.
 rewrite ?Z.max_r by lia.
-rewrite sublist_nil, <- app_nil_end by lia.
+rewrite sublist_nil, app_nil_r by lia.
 auto.
 Qed.
 *)
@@ -143,7 +143,7 @@ Proof.
  try (rewrite ?Zlength_correct; lia).
 rewrite ?Z.min_l by lia.
 rewrite ?Z.max_r by lia.
-rewrite sublist_nil, <- app_nil_end by lia.
+rewrite sublist_nil, app_nil_r by lia.
 rewrite sublist_same; auto.
 rewrite Zlength_sublist; lia.
 Qed.
@@ -157,7 +157,7 @@ Lemma part3_splice_into_list:
 Proof.
  intros.
  unfold splice_into_list.
-rewrite <- app_ass.
+rewrite app_assoc.
  rewrite (sublist_app); rewrite ?Zlength_repeat, ?Z.max_r, ?Z.max_l by lia; try lia;
  rewrite ?Zlength_sublist by lia;
  try (rewrite ?Zlength_correct; lia).
diff --git a/sha/pure_lemmas.v b/sha/pure_lemmas.v
index 992982427..b5b944614 100644
--- a/sha/pure_lemmas.v
+++ b/sha/pure_lemmas.v
@@ -354,14 +354,14 @@ unfold lastblock'.
 rewrite bytelist_to_intlist_to_bytelist; auto.
 2: rewrite H99; exists LBLOCKz; reflexivity.
 unfold lastblock.
-rewrite <- app_ass. rewrite H5.
+rewrite app_assoc. rewrite H5.
 unfold generate_and_pad.
 rewrite intlist_to_bytelist_app.
 rewrite bytelist_to_intlist_to_bytelist; auto.
 *
-repeat rewrite app_ass.
+repeat rewrite <- app_assoc.
 f_equal. f_equal. f_equal.
-rewrite <- app_ass.
+rewrite app_assoc.
 f_equal.
 rewrite <- repeat_app.
 f_equal.
@@ -375,7 +375,7 @@ rewrite Z.mul_comm.
 rewrite <-  Zlength_intlist_to_bytelist.
 rewrite <- Zlength_app.
 rewrite H5.
-rewrite <- app_ass.
+rewrite app_assoc.
 rewrite Zlength_app.
 forget (Zlength (intlist_to_bytelist hashed ++ dd)) as B.
 rewrite Zlength_app.
diff --git a/sha/sha_lemmas.v b/sha/sha_lemmas.v
index f44632bca..3831f93c1 100644
--- a/sha/sha_lemmas.v
+++ b/sha/sha_lemmas.v
@@ -567,7 +567,7 @@ split.
    rewrite sublist_app2 by lia.
    autorewrite with sublist.
    rewrite (sublist_same 0) by lia.
-   rewrite <- app_ass. f_equal.
+   rewrite app_assoc. f_equal.
    rewrite sublist_rejoin; try lia. auto.
    split. apply round_range; apply CBLOCKz_gt.
  apply Zmult_le_compat_r; [ | rewrite CBLOCKz_eq; lia].
@@ -582,7 +582,7 @@ split.
  -
    rewrite (sublist_split (Zlength a / CBLOCKz * CBLOCKz) (Zlength a)
                   (Zlength (a ++ msg) / CBLOCKz * CBLOCKz) ); auto.
-   rewrite app_ass.
+   rewrite <- app_assoc.
    rewrite sublist_app1; try lia.
    rewrite sublist_app2; try lia.
    rewrite Z.sub_diag.
@@ -603,13 +603,13 @@ match type of H4 with ?A = ?B =>
               sublist 0 (Zlength a / CBLOCKz * CBLOCKz) a ++ B) by congruence
 end.
 unfold s256a_hashed, s256a_data in *.
-rewrite <- app_ass in H6.
+rewrite app_assoc in H6.
 rewrite sublist_rejoin in H6 by lia.
 rewrite sublist_same in H6 by lia.
 rewrite H6.
 clear H6 H4.
 rewrite <- (sublist_same 0 (Zlength a') a') at 1; auto.
-rewrite <- app_ass.
+rewrite app_assoc.
 rewrite (sublist_split 0 (Zlength a' / CBLOCKz * CBLOCKz) (Zlength a')); try lia.
 f_equal.
 apply bytelist_to_intlist_inj.
diff --git a/sha/verif_hmac_final.v b/sha/verif_hmac_final.v
index 35df41584..a54eb641d 100644
--- a/sha/verif_hmac_final.v
+++ b/sha/verif_hmac_final.v
@@ -145,7 +145,7 @@ Time forward_call (oSha, SHA256.SHA_256 ctx, Vptr b i, wsh, buf, Tsh, Z.of_nat S
 *)
      Time cancel. (*0.2 versus 1.6*) }
   { unfold SHA256.DigestLength.
-    rewrite oShaLen. simpl; intuition. }
+    rewrite oShaLen. simpl; intuition auto with *. }
 simpl.
 rewrite sublist_same; try lia.
 unfold sha256state_. Intros updShaST.
diff --git a/sha/verif_sha_final2.v b/sha/verif_sha_final2.v
index f8c7e3804..901d593e5 100644
--- a/sha/verif_sha_final2.v
+++ b/sha/verif_sha_final2.v
@@ -201,8 +201,8 @@ replace_SEP 0  (data_at wsh t_struct_SHA256state_st
  unfold data_at.
  go_lower; simpl; cancel. (* saturate_local makes entailer! is REALLY slow, but (go_lower; cancel) is fast. *)
  change (cons (Vint (Int.repr 128))) with (app [Vint (Int.repr 128)]).
- rewrite <- !(app_ass _ [_]).
- rewrite <- app_nil_end.
+ rewrite !(app_assoc _ [_]).
+ rewrite app_nil_r.
  rewrite field_at_data_at with (gfs := [StructField _data]) by reflexivity.
  eapply cancel_field_at_array_partial_undef; try reflexivity; try apply JMeq_refl.
  autorewrite with sublist. lia.
@@ -253,7 +253,7 @@ replace (splice_into_list (ddlen + 1) CBLOCKz
  clear - Hddlen. subst ddz fill_len ddlen. rewrite !map_app.
  change (cons (Vint (Int.repr 128))) with (app [Vint (Int.repr 128)]).
  rewrite map_repeat.
- rewrite <- ?app_ass.
+ rewrite ?app_assoc.
  unfold splice_into_list.
  change CBLOCKz with 64 in *.
  autorewrite with sublist. reflexivity. 
@@ -293,7 +293,7 @@ forward_call (* sha256_block_data_order (c,p); *)
   rewrite !map_app.
   unfold splice_into_list.
   autorewrite with sublist.
-  rewrite <- (app_ass (map Vubyte dd)).
+  rewrite (app_assoc (map Vubyte dd)).
   autorewrite with sublist.
   reflexivity.
 }
@@ -312,7 +312,7 @@ split.
   f_equal.
   rewrite <- HU.
   repeat rewrite map_app.
-  repeat rewrite app_ass.
+  repeat rewrite <- app_assoc.
  f_equal.
 *
  unfold_data_at (data_at _ _ _ _).
diff --git a/sha/verif_sha_final3.v b/sha/verif_sha_final3.v
index e236cdd84..5a914fc14 100644
--- a/sha/verif_sha_final3.v
+++ b/sha/verif_sha_final3.v
@@ -375,11 +375,11 @@ Proof.
   erewrite field_at_Tarray;
    [ | apply compute_legal_nested_field_spec'; repeat constructor; auto; lia
    | reflexivity | lia | apply JMeq_refl].
-  rewrite <- app_ass.
+  rewrite app_assoc.
    change (Z.to_nat 8) with (Z.to_nat 4 + Z.to_nat 4)%nat.
    rewrite repeat_app.
    rewrite (split3seg_array_at _ _ _ 0 56 60) by (autorewrite with sublist; rep_lia).
-   rewrite <- !app_ass.
+   rewrite !app_assoc.
    assert (CBZ := CBLOCKz_eq).
    Time autorewrite with sublist. (*7*)
     clear CBZ.
@@ -436,7 +436,7 @@ Proof.
    rewrite (split3seg_array_at _ _ _ 0 56 60 64)
      by (autorewrite with sublist; lia).
    rewrite CBLOCKz_eq in *.
-   rewrite <- !app_ass.
+   rewrite !app_assoc.
    Time autorewrite with sublist. (*7*)
    change (64-8) with 56.
    rewrite (array_at_data_at' _ _ _ 56 60) by auto.
diff --git a/sha/verif_sha_update.v b/sha/verif_sha_update.v
index e3d6f05d2..ece454f56 100644
--- a/sha/verif_sha_update.v
+++ b/sha/verif_sha_update.v
@@ -141,7 +141,7 @@ assert (UAE: S256abs (hashed ++ blocks) (sublist b4d len data) =
  rewrite !S256abs_hashed
    by (try apply divide_length_app; auto; autorewrite with sublist; auto).
  split; auto.
- rewrite Hblocks. rewrite app_ass.
+ rewrite Hblocks. rewrite <- app_assoc.
  rewrite !S256abs_data
    by (try apply divide_length_app; auto; autorewrite with sublist; auto).
  f_equal.
diff --git a/sha/verif_sha_update3.v b/sha/verif_sha_update3.v
index b6eb6cd72..d1dc2b850 100644
--- a/sha/verif_sha_update3.v
+++ b/sha/verif_sha_update3.v
@@ -135,9 +135,9 @@ Proof.
   intros.
     assert (Zlength (dd ++ sublist 0 len data) < CBLOCKz). 
      change CBLOCKz with 64. list_solve.
-    rewrite (app_nil_end hashed) at 2.
+    rewrite <- (app_nil_r hashed) at 2.
     rewrite update_abs_eq.
-    exists nil. rewrite <- !app_nil_end.
+    exists nil. rewrite !app_nil_r.
     rewrite !S256abs_hashed; auto.
     rewrite !S256abs_data; auto.
 Qed.
diff --git a/sha/verif_sha_update4.v b/sha/verif_sha_update4.v
index 4e0026afa..82270750d 100644
--- a/sha/verif_sha_update4.v
+++ b/sha/verif_sha_update4.v
@@ -111,7 +111,7 @@ forward.
 apply andp_left2; auto.
 * (* else clause *)
 forward.  (* skip; *)
-Exists (@nil int). rewrite <- app_nil_end.
+Exists (@nil int). rewrite app_nil_r.
 rename H0 into H1.
 rewrite H1 in *.
 rewrite Zlength_correct in H1;  destruct dd; inv H1.
@@ -267,7 +267,7 @@ assert (Zlength bl = LBLOCKz). {
   + rewrite H7; apply Z.divide_add_r; auto. apply Z.divide_refl.
   + rewrite intlist_to_bytelist_app.
       rewrite Hblocks; rewrite <- H6.
-      rewrite app_ass.
+      rewrite <- app_assoc.
       f_equal.
       rewrite <- sublist_split; try Omega1.
       f_equal. Omega1.
@@ -281,7 +281,7 @@ assert (Zlength bl = LBLOCKz). {
  Time unfold_data_at (data_at _ _ _ c).  (*0.8*)
  rewrite (split3_data_block lo (lo+CBLOCKz) sh data d)
     by (auto; subst lo; try Omega1).
- rewrite app_ass.
+ rewrite <- app_assoc.
  rewrite H6.
  Time cancel. (*1.2*)
  }
diff --git a/tweetnacl20140427/verif_crypto_stream_salsa20_xor1.v b/tweetnacl20140427/verif_crypto_stream_salsa20_xor1.v
index 074955d3c..6fc506769 100644
--- a/tweetnacl20140427/verif_crypto_stream_salsa20_xor1.v
+++ b/tweetnacl20140427/verif_crypto_stream_salsa20_xor1.v
@@ -66,7 +66,7 @@ Proof. intros.
   apply Z_to_nat_monotone. lia.
   rewrite ZtoNat_Zlength. lia.
   replace (sublist a (a+b) l) with (@nil A).
-  rewrite <- app_nil_end.
+  rewrite app_nil_r.
   unfold sublist. f_equal.
   rewrite !firstn_same; auto.
   rewrite <- ZtoNat_Zlength.
diff --git a/tweetnacl20140427/verif_salsa_base.v b/tweetnacl20140427/verif_salsa_base.v
index 793a16230..8f211e64d 100644
--- a/tweetnacl20140427/verif_salsa_base.v
+++ b/tweetnacl20140427/verif_salsa_base.v
@@ -92,13 +92,13 @@ Lemma ThirtyTwoByte_split16 q v:
 Proof. destruct q as [s1 s2]. simpl; intros. unfold SByte.
   rewrite split2_data_at_Tarray_tuchar with (n1:= Zlength (SixteenByte2ValList s1));
      try rewrite Zlength_app; repeat rewrite <- SixteenByte2ValList_Zlength; try lia.
-  unfold offset_val. red in H. destruct v; intuition.
+  unfold offset_val. red in H. destruct v; intuition auto with *.
   rewrite field_address0_offset. simpl.
   rewrite sublist_app1; try rewrite <- SixteenByte2ValList_Zlength; try lia.
   rewrite sublist_app2; try rewrite <- SixteenByte2ValList_Zlength; try lia.
   rewrite sublist_same; try rewrite <- SixteenByte2ValList_Zlength; trivial.
   rewrite sublist_same; try rewrite <- SixteenByte2ValList_Zlength; trivial.
-  red; intuition.
+  red; intuition auto with *.
 Qed.
 
 Lemma QuadByte2ValList_firstn4 q l:
diff --git a/veric/SequentialClight.v b/veric/SequentialClight.v
index c3e74e45b..742d89ff0 100644
--- a/veric/SequentialClight.v
+++ b/veric/SequentialClight.v
@@ -429,7 +429,7 @@ Proof.
       rewrite <- Heq.
       destruct (access_at m loc Cur); auto.
       destruct p; auto.
-  - revert dependent m; induction l; simpl; intros.
+  - generalize dependent m; induction l; simpl; intros.
     + inv H; destruct (access_at m' loc Cur); auto.
       destruct p; auto.
     + destruct a as ((b, lo), hi).
@@ -800,7 +800,7 @@ Lemma add_funspecs_frame' : forall {Espec : OracleKind} extlink fs,
   extspec_frame OK_spec -> extspec_frame (@OK_spec (add_funspecs Espec extlink fs)).
 Proof.
   destruct Espec; simpl; intros.
-  revert dependent OK_spec; induction fs; simpl; auto; intros.
+  generalize dependent OK_spec; induction fs; simpl; auto; intros.
   destruct a; apply funspec2jspec_frame; auto.
 Qed.
 
diff --git a/veric/SequentialClight2.v b/veric/SequentialClight2.v
index cb2016a64..39378bd6d 100644
--- a/veric/SequentialClight2.v
+++ b/veric/SequentialClight2.v
@@ -425,7 +425,7 @@ Proof.
       rewrite <- Heq.
       destruct (access_at m loc Cur); auto.
       destruct p; auto.
-  - revert dependent m; induction l; simpl; intros.
+  - generalize dependent m; induction l; simpl; intros.
     + inv H; destruct (access_at m' loc Cur); auto.
       destruct p; auto.
     + destruct a as ((b, lo), hi).
@@ -796,7 +796,7 @@ Lemma add_funspecs_frame' : forall {Espec : OracleKind} extlink fs,
   extspec_frame OK_spec -> extspec_frame (@OK_spec (add_funspecs Espec extlink fs)).
 Proof.
   destruct Espec; simpl; intros.
-  revert dependent OK_spec; induction fs; simpl; auto; intros.
+  generalize dependent OK_spec; induction fs; simpl; auto; intros.
   destruct a; apply funspec2jspec_frame; auto.
 Qed.
 
diff --git a/veric/age_to_resource_at.v b/veric/age_to_resource_at.v
index 65bec5282..b12676f0d 100644
--- a/veric/age_to_resource_at.v
+++ b/veric/age_to_resource_at.v
@@ -116,7 +116,7 @@ Proof.
   pose proof (age_to_ageN n phi).
   forget (age_to n phi) as phi'.
   remember (level phi - n) as n'.
-  revert dependent n; revert dependent phi; induction n'; intros.
+  generalize dependent n; generalize dependent phi; induction n'; intros.
   - inv H.
     rewrite <- ghost_of_approx, ghost_fmap_fmap, approx'_oo_approx, approx_oo_approx' by lia; auto.
   - change (ageN (S n') phi) with
diff --git a/veric/initialize.v b/veric/initialize.v
index 874eb74b7..558d724b4 100644
--- a/veric/initialize.v
+++ b/veric/initialize.v
@@ -1114,7 +1114,7 @@ assert (forall loc, fst loc <> b -> identity (phi @ loc)).
       pose proof (init_data_size_pos a); pose proof max_unsigned_modulus; lia).
   apply IHdl; auto.
   apply andb_true_iff in AL; destruct AL; auto.
-  rewrite app_ass; auto.
+  rewrite <- app_assoc; auto.
   intro loc; specialize (H6 loc); specialize (H8 loc); specialize (H4 loc).
   if_tac. rewrite if_true in H4; auto.
   destruct loc; destruct H11; auto.
@@ -1410,7 +1410,7 @@ simpl in *.
 destruct G; inv H0. apply H1.
 destruct a.
 inv H0.
-simpl. do 2 rewrite app_ass.
+simpl. do 2 rewrite <- app_assoc.
 simpl.
 apply IHvl.
 clear - H.
@@ -1450,17 +1450,17 @@ Lemma match_fdecs_rev:
 Proof.
   intros; apply prop_ext; split; intros.
 *
-  rewrite (app_nil_end vl).
-  rewrite (app_nil_end G).
+  rewrite <- (app_nil_r vl).
+  rewrite <- (app_nil_r G).
   rewrite <- (rev_involutive vl), <- (rev_involutive G).
   apply match_fdecs_rev'; auto.
-  rewrite rev_involutive, <- app_nil_end; auto.
+  rewrite rev_involutive, app_nil_r; auto.
   constructor.
 *
-  rewrite (app_nil_end (rev vl)).
-  rewrite (app_nil_end (rev G)).
+  rewrite <- (app_nil_r (rev vl)).
+  rewrite <- (app_nil_r (rev G)).
   apply match_fdecs_rev'; auto.
-  rewrite <- app_nil_end.
+  rewrite app_nil_r.
   rewrite map_rev. rewrite list_norepet_rev; auto.
   constructor.
 Qed.
@@ -2110,7 +2110,7 @@ rewrite Pos_to_nat_eq_S.
   right; auto.
   assert (FI: find_id i (G0++G) = None). {
   change (list_norepet (map fst G0 ++ (i::nil) ++ (map fst vl))) in H2.
-  apply list_norepet_append_commut in H2. rewrite app_ass in H2.
+  apply list_norepet_append_commut in H2. rewrite <- app_assoc in H2.
  inv H2. specialize (H1 i).
  case_eq (find_id i (G0++G)); intros; auto. apply find_id_e in H2.
  contradiction H6. apply in_app. apply in_app_or in H2.
diff --git a/veric/invariants.v b/veric/invariants.v
index 3146dc7d3..314eeb5de 100644
--- a/veric/invariants.v
+++ b/veric/invariants.v
@@ -404,7 +404,7 @@ Proof.
       destruct H, H0; split; auto; lia.
   - intro a.
     remember (length a) as n.
-    revert dependent a; induction n; intros.
+    generalize dependent a; induction n; intros.
     + destruct a; inv Heqn.
       exists b; split; auto.
       change [] with (core b); apply core_unit.
diff --git a/veric/juicy_extspec.v b/veric/juicy_extspec.v
index 317699b56..a7b3fd880 100644
--- a/veric/juicy_extspec.v
+++ b/veric/juicy_extspec.v
@@ -521,7 +521,7 @@ Proof.
     + eapply rt_trans; eauto.
   - intros [].
     remember (m_phi m1) as jm1; remember (m_phi m2) as jm2.
-    revert dependent m2; revert dependent m1.
+    generalize dependent m2; generalize dependent m1.
     induction H0; intros; subst; auto.
     + constructor.
       apply age1_juicy_mem_unpack''; auto.
@@ -820,7 +820,7 @@ Lemma ext_safe:
 Proof.
   intros ????? Hext ?.
   remember (level jm0) as N.
-  revert dependent c; revert dependent jm0; revert dependent jm; induction N as [? IHN] using lt_wf_ind; intros.
+  generalize dependent c; generalize dependent jm0; generalize dependent jm; induction N as [? IHN] using lt_wf_ind; intros.
   inv H0.
   - constructor. destruct H as [_ H]; apply rmap_order in H as [? _].
     rewrite <- !level_juice_level_phi in *; congruence.
diff --git a/veric/rmaps.v b/veric/rmaps.v
index fdc1d104d..7e84d6f34 100644
--- a/veric/rmaps.v
+++ b/veric/rmaps.v
@@ -528,7 +528,7 @@ Module StratModel (AV' : ADR_VAL) : STRAT_MODEL with Module AV:=AV'.
       inv H; constructor; auto.
       inv H1; constructor; auto.
       inv H2; constructor; auto; simpl; congruence.
-    - revert dependent z; revert y; induction x'; intros; apply ghost_join_inv in H.
+    - generalize dependent z; revert y; induction x'; intros; apply ghost_join_inv in H.
       { exists nil, z; split; auto; constructor. }
       destruct y; simpl in *.
       { exists z, nil; split; auto; constructor. }
@@ -562,7 +562,7 @@ Module StratModel (AV' : ADR_VAL) : STRAT_MODEL with Module AV:=AV'.
         unfold ghost_fmap in *; simpl in *.
         rewrite <- H1; f_equal.
         destruct o, o0; inv J1; auto.
-    - revert dependent z'; revert y; induction x; intros; apply ghost_join_inv in H; simpl in H.
+    - generalize dependent z'; revert y; induction x; intros; apply ghost_join_inv in H; simpl in H.
       { exists y, y; split; auto; constructor. }
       destruct y; simpl in *.
       { exists nil, (a :: x); split; auto; constructor. }
@@ -1504,7 +1504,7 @@ Qed.
       destruct f, f0, f1; simpl in *.
       clear - H2.
       remember (g2ghost g) as a; remember (g2ghost g0) as b; remember (g2ghost g1) as c.
-      revert dependent g1; revert dependent g0; revert dependent g; induction H2; intros; subst.
+      generalize dependent g1; generalize dependent g0; generalize dependent g; induction H2; intros; subst.
       * apply g2ghost_inv in Heqc; subst; destruct g; [constructor | discriminate].
       * apply g2ghost_inv in Heqc; subst; destruct g0; [constructor | discriminate].
       * destruct g, g0, g1; inv Heqa; inv Heqb; inv Heqc.
@@ -1635,10 +1635,10 @@ Qed.
       unfold res2resource in Hr.
       destruct (_f l), (_f1 l); try destruct _f3; try destruct _f4; inv Hr; f_equal; try apply proof_irr.
     - match goal with J : join ?a _ ?c |- _ => remember a as g1; remember c as g2 end.
-      revert dependent _f0. revert dependent _f2. induction J; intros; subst.
+      generalize dependent _f0. generalize dependent _f2. induction J; intros; subst.
       + destruct _f0; inv Heqg1; eexists; constructor.
       + assert (_f2 = _f0); [|subst; eexists; constructor].
-        clear - Heqg1. revert dependent _f2; induction _f0; intros; destruct _f2; inv Heqg1; auto.
+        clear - Heqg1. generalize dependent _f2; induction _f0; intros; destruct _f2; inv Heqg1; auto.
         f_equal; [|apply IH_f0; auto].
         destruct o as [(?, (?, ?))|], a as [(?, (?, ?))|]; inv H0; auto.
       + destruct _f0; inv Heqg1. destruct _f2; inv Heqg2.
diff --git a/veric/rmaps_lemmas.v b/veric/rmaps_lemmas.v
index 08bb41fba..80f36c5db 100644
--- a/veric/rmaps_lemmas.v
+++ b/veric/rmaps_lemmas.v
@@ -213,7 +213,7 @@ Proof.
   destruct r.
   simpl in H1; destruct H1.
   remember (ghost_fmap (approx n) (approx n) g0) as g'.
-  revert dependent g0; induction H; auto; intros; subst.
+  generalize dependent g0; induction H; auto; intros; subst.
   - rewrite ghost_fmap_fmap, approx_oo_approx; auto.
   - destruct g0; inv Heqg'.
     simpl; f_equal; eauto.
@@ -328,7 +328,7 @@ Lemma ghost_same_level_gen:
 Proof.
   intros.
   remember (ghost_fmap (approx n) (approx n) a) as a'; remember (ghost_fmap (approx n) (approx n) b) as b'.
-  revert dependent b; revert dependent a; induction H; intros; subst.
+  generalize dependent b; generalize dependent a; induction H; intros; subst.
   - rewrite ghost_fmap_fmap, approx_oo_approx; auto.
   - rewrite ghost_fmap_fmap, approx_oo_approx; auto.
   - destruct a, b; inv Heqa'; inv Heqb'.
diff --git a/veric/semax_lemmas.v b/veric/semax_lemmas.v
index c6029e9a4..11c688500 100644
--- a/veric/semax_lemmas.v
+++ b/veric/semax_lemmas.v
@@ -771,7 +771,7 @@ Lemma safe_loop_skip:
 Proof.
   intros.
   remember (level m) as M.
-  revert dependent m; induction M as [? IHM] using lt_wf_ind; intros.
+  generalize dependent m; induction M as [? IHM] using lt_wf_ind; intros.
   eapply jsafeN_local_step. constructor.
   intros.
   eapply jsafeN_local_step. constructor. auto.
diff --git a/veric/semax_prog.v b/veric/semax_prog.v
index f12c04ba2..f8d2827aa 100644
--- a/veric/semax_prog.v
+++ b/veric/semax_prog.v
@@ -2701,7 +2701,7 @@ Proof.
   repeat split; auto; intro.
   - destruct (PTree.get _ _); auto.
   - unfold make_tycontext_g.
-    revert dependent G2; revert dependent V2; revert V; induction G; simpl.
+    generalize dependent G2; generalize dependent V2; revert V; induction G; simpl.
     + induction V; simpl; intros. auto.
         rewrite sublist.incl_cons_iff in HV; destruct HV.
         rewrite PTree.gsspec.
@@ -2716,7 +2716,7 @@ Proof.
       destruct (peq id (fst a)); eauto; subst; simpl.
       apply lookup_distinct; auto.
   - unfold make_tycontext_s.
-    revert dependent G2; induction G; simpl; intros.
+    generalize dependent G2; induction G; simpl; intros.
     + auto.
     + destruct a; simpl. hnf.
       rewrite sublist.incl_cons_iff in HG; destruct HG.
diff --git a/veristar/isolate_sound.v b/veristar/isolate_sound.v
index bf6db5bc1..b6a637cf5 100644
--- a/veristar/isolate_sound.v
+++ b/veristar/isolate_sound.v
@@ -491,11 +491,11 @@ split; auto.
 left.
 eapply Lseg_unfold_neq with e0; auto.
 simpl in H.
-rewrite app_ass in H; apply H.
+rewrite <- app_assoc in H; apply H.
 (*repeat rewrite list_denote_separate.*)
 rewrite (@listd_prop pn_atom state pn_atom_denote).
 split; auto.
-rewrite app_ass in HypSig; apply HypSig.
+rewrite <- app_assoc in HypSig; apply HypSig.
 intros.
 simpl in H4.
 destruct H4.
@@ -534,7 +534,7 @@ simpl; intros.
 revert H0; case_eq (incon (Assertion pnatoms (rev sigma0))); intros; inv H1.
 apply incon_e in H0.
 split.
-rewrite <- app_nil_end.
+rewrite app_nil_r.
 eapply derives_trans; [apply H0 | auto].
 simpl; intros; contradiction.
 Qed.
@@ -562,7 +562,7 @@ revert H0; case_eq (exorcize e (Equ e0 e1 :: pnatoms) (Lseg e0 e1 :: sigma0) sig
   intros; inv H1.
 left; split; auto.
 apply oracle_sound in H; simpl in H.
-rewrite app_ass. auto.
+rewrite <- app_assoc. auto.
 exists l; split; auto.
 right. auto.
 Qed.
@@ -796,7 +796,7 @@ remember O as N. clear HeqN.
 revert pnatoms sigma0 results N H H0; induction sigma; intros.
 
 (* nil case *)
-rewrite <- app_nil_end in *;
+rewrite app_nil_r in *;
 unfold isolate' in H.
 apply exorcize_sound; auto.
 destruct (lt_dec N 2) as [? | _];  [ inversion H | ].
@@ -824,11 +824,11 @@ apply isolate_Next2; auto; apply oracle_sound; auto.
 specialize (IHsigma _ H4); clear H4.
 destruct IHsigma.
 change (rev (Next e0 e1 :: sigma0)) with (rev sigma0 ++ [Next e0 e1]).
-rewrite app_ass. apply H0.
+rewrite <- app_assoc. apply H0.
 split; auto.
 eapply derives_trans; try apply H.
 simpl.
-rewrite app_ass. auto.
+rewrite <- app_assoc. auto.
 
 (* 'Lseg' case *)
 apply isolate_e in H.
@@ -838,12 +838,12 @@ subst.
 apply isolate_Lseg1; auto.
 
 change (rev (Lseg e0 e1 :: sigma0)) with (rev sigma0 ++ [Lseg e0 e1]) in *.
-rewrite app_ass in *.
+rewrite <- app_assoc in *.
 simpl in *.
 apply (IHsigma _ H1); auto.
 
 change (rev (Lseg e0 e1 :: sigma0)) with (rev sigma0 ++ [Lseg e0 e1]) in *.
-rewrite app_ass in IHsigma.
+rewrite <- app_assoc in IHsigma.
 apply (IHsigma _ H); auto.
 Qed.
 
diff --git a/veristar/redblack.v b/veristar/redblack.v
index 18f413497..66c3b75e5 100644
--- a/veristar/redblack.v
+++ b/veristar/redblack.v
@@ -3929,7 +3929,7 @@ Qed.
   pattern l at 2; replace l with (rev l) by (subst; simpl; auto).
   clear.
   revert l; induction s; simpl; intros; auto.
-  rewrite <- app_nil_end. symmetry; apply rev_involutive.
+  rewrite app_nil_r. symmetry; apply rev_involutive.
   rewrite IHs2. rewrite IHs1.
   clear.
   remember ( fold' (list key) (@cons _) s1 nil) as B.
@@ -3941,7 +3941,7 @@ Qed.
   clear.
   simpl.
   rewrite rev_involutive.
-  repeat rewrite app_ass.
+  repeat rewrite <- app_assoc.
   simpl; auto.
 Qed.
 
diff --git a/zlist/sublist.v b/zlist/sublist.v
index 2e4082cab..505f65077 100644
--- a/zlist/sublist.v
+++ b/zlist/sublist.v
@@ -1165,7 +1165,7 @@ rewrite (Z.min_l lo (Zlength al)) by lia.
 rewrite (Z.max_r (hi-Zlength al) 0) by lia.
 rewrite (Z.max_r (lo-Zlength al) 0) by lia.
 simpl firstn.
-rewrite <- app_nil_end.
+rewrite app_nil_r.
 rewrite Zskipn_app1 by lia.
 rewrite Zfirstn_app1
  by (rewrite Zlength_skipn, !Z.max_r; try lia;
@@ -1608,7 +1608,7 @@ Qed.
 #[export] Hint Rewrite @Zlength_cons @Zlength_nil: sublist.
 #[export] Hint Rewrite @Zrepeat_neg using lia : sublist.
 #[export] Hint Rewrite @repeat_0 @Zrepeat_0: sublist.
-#[export] Hint Rewrite <- @app_nil_end : sublist.
+#[export] Hint Rewrite @app_nil_r : sublist.
 #[export] Hint Rewrite @Zlength_app: sublist.
 #[export] Hint Rewrite @Zlength_map: sublist.
 #[export] Hint Rewrite @Zlength_Zrepeat using old_list_solve: sublist.
@@ -1695,7 +1695,7 @@ Lemma sublist_one:
 Proof.
 intros.
 subst.
-rewrite Znth_cons_sublist by lia. rewrite <- app_nil_end.
+rewrite Znth_cons_sublist by lia. rewrite app_nil_r.
 auto.
 Qed.
 
@@ -2217,7 +2217,7 @@ Qed.
 Lemma Forall2_sublist : forall {A B} (P : A -> B -> Prop) l1 l2 i j, Forall2 P l1 l2 -> 0 <= i ->
   Forall2 P (sublist i j l1) (sublist i j l2).
 Proof.
-  intros; revert j; revert dependent i; induction H; intros.
+  intros; revert j; generalize dependent i; induction H; intros.
   - rewrite !sublist_of_nil; constructor.
   - destruct (Z_le_dec j i); [rewrite !sublist_nil_gen; auto; constructor|].
     destruct (Z.eq_dec i 0).