Update release notes; tweak a coq-dev compatibility issue

floyd/printf.v

@@ -140,14 +140,16 @@ Proof.
   eapply Z.lt_le_trans, Z_mult_div_ge with (b := 10); lia.
 Defined.
 
+Import Wf.
+
 Lemma chars_of_Z_eq : forall n, chars_of_Z n =
   match n <? 0 with true => charminus :: chars_of_Z (Z.abs n) | false =>
   let n' := n / 10 in
   match n' <=? 0 with true => [Byte.repr (n + char0)] | false => chars_of_Z n' ++ [Byte.repr (n mod 10 + char0)] end end.
 Proof.
   intros.
   unfold chars_of_Z at 1.
-  rewrite Wf.WfExtensionality.fix_sub_eq_ext; simpl; fold chars_of_Z.
+  rewrite WfExtensionality.fix_sub_eq_ext; simpl; fold chars_of_Z.
   destruct (_ <? _); auto.
   destruct (_ <=? _); auto.
 Qed.

util/RELEASE

@@ -1,11 +1,31 @@
 How to generate a release:
 
-1. cd .../vst; git tag -a vX.Y -m "VST release X.Y"; git push origin vX.Y
-2. In a fork of the opam-coq-archive,
-      https://github.com/coq/opam
-   within directory released/packages/coq-vst
+1. Before tagging a new release of VST, it is suggested (but not required) to make sure that VSTlib  is up to date. To do that:
+   1.1  in vst directory, "make install"
+   1.2  make and install vcfloat
+   1.3  cd vst/lib, "make"  (which depends on vst and vcfloat being installed)
+   1.4  fix anything that needs fixing, and commit changes to the vst repo.
 
+2. in the vst repo:
+   2.1   git tag -a vX.Y -m "VST release X.Y"; git push origin vX.Y
+   2.2   in github, click the button to turn this tag into a release
+   2.3   download https://github.com/PrincetonUniversity/VST/archive/refs/tags/vX.Y.tar.gz
+   2.3   shasum -a 256 vX.Y.tar.gz
 
+3. In a fork of the opam-coq-archive,
+      https://github.com/coq/opam
+   3.1 create   released/packages/coq-vst/coq-vst.X.Y/opam  
+   3.2  edit the opam file, using the result of the shasum command above
+   3.3 create   released/packages/coq-vst/coq-vst-lib.X.Y/opam  
+   3.4  edit the opam file, using the result of the shasum command above
+       [note: "src" and "checksum" of VST and VSTlib are the same]
+   3.5a If the vst/zlist files have NOT been modified, then just
+         edit the last coq-vst-zlist/coq-vst-zlist.A.B/opam
+	to indicate compatibility with the current Coq version
+   3.5b If the vst/zlist files have been modified, then create
+         a new release of coq-vst-zlist; like coq-vst-lib it shares
+	 a "src" and "checksum" with VST.
+   3.6  "git add" the new opam files and commit to the fork
 
 ---------THE FOLLOWING INSTRUCTIONS ARE OBSOLETE, from before opam--------
 ***** reminder about how to generate a release