From 273095efe710550df5bd16348242d6704190cdc8 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 29 May 2018 12:31:39 +0100
Subject: Add missing Coq builtin info to vector_inc

---
 lib/vector_inc.sail | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail
index 1db466db..c45fec6b 100644
--- a/lib/vector_inc.sail
+++ b/lib/vector_inc.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 >= 0 & 'm <= 'n. (vector('n, inc, bit), atom('m)) -> vector('m, inc, bit)
 
-- 
cgit v1.2.3