Support Coq 8.15, 8.16 in support libraries

This requires a small change from `Numeral Notation` notation to `Number
Notation`, the former of which was removed in Coq 8.15. The latter is only
supported in Coq 8.13 or later, so I have documented this in the `saw-core-coq`
`README`.

Fixes #1601.

saw-core-coq/README.md

@@ -33,10 +33,14 @@ opam repo add coq-released https://coq.inria.fr/opam/released
 opam install coq-bits
 ```
 
-If you run into any issue that is probably due to the version mismatch between the `ocamlc` 
-and the `ocaml` base system installed on your machine and it can be fixed as explained 
+If you run into any issue that is probably due to the version mismatch between the `ocamlc`
+and the `ocaml` base system installed on your machine and it can be fixed as explained
 [here](https://github.com/ocaml/opam/issues/3708).
 
+Currently, the Coq support libraries for `saw-core-coq` requires Coq 8.13 or
+later.  In particular, they are known to build with Coq 8.13, 8.15, and 8.16,
+but *not* 8.14 (see [this
+issue](https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Code.20typechecks.20in.20Coq.208.2E13.2C.20but.20not.20in.208.2E14)).
 
 ## Building the and Using the Coq Support Libraries
 

saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v

@@ -230,7 +230,7 @@ Definition sbvToInt (n : Nat) (b : bitvector n) : Z
 
 (* Useful notation for bools *)
 Definition boolToInt (b : bool) : Z := if b then 1%Z else 0%Z.
-Numeral Notation bool Z.odd boolToInt : bool_scope.
+Number Notation bool Z.odd boolToInt : bool_scope.
 Close Scope bool_scope. (* no, don't interpret all numbers as booleans... *)
 
 (* This is annoying to implement, so using BITS conversion *)