Merge branch 'sail2' into mappings

1 files changed, 4 insertions, 1 deletions

diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index eb2c9b7e..17603e03 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -15,7 +15,7 @@ val eq_bits = {
 
 overload operator == = {eq_bit, eq_bits}
 
-val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
+val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. bits('n) -> atom('n)
 
 val vector_length = {
   ocaml: "length",
@@ -36,6 +36,7 @@ val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
 val truncate = {
   ocaml: "vector_truncate",
   lem: "vector_truncate",
+  coq: "vector_truncate",
   c: "truncate"
 } : forall 'm 'n, 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit)
 
@@ -67,11 +68,13 @@ val vector_update = {
 
 val add_bits = {
   ocaml: "add_vec",
+  lem: "add_vec",
   c: "add_bits"
 } : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 val add_bits_int = {
   ocaml: "add_vec_int",
+  lem: "add_vec_int",
   c: "add_bits_int"
 } : forall 'n. (bits('n), int) -> bits('n)