From 7cdbee76d454047271ef6cdaa82a2b7e2ed590ba Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 7 Jun 2018 18:00:59 +0100
Subject: Coq: add destructuring of atom existentials in patterns Plus test
 case, broken builtin name

---
 lib/vector_dec.sail | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 60f49af8..d9b80b32 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -122,7 +122,7 @@ val unsigned = {
   lem: "uint",
   interpreter: "uint",
   c: "sail_uint",
-  coq: "uint"
+  coq: "unsigned"
 } : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
 
 val signed = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
-- 
cgit v1.2.3