From 92f50f2564834fcbeda250337c3acce571f7d6f0 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Tue, 16 Jul 2019 22:12:42 +0100
Subject: Fix all remaining tests for this branch

---
 src/initial_check.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'src/initial_check.ml')

diff --git a/src/initial_check.ml b/src/initial_check.ml
index f41033ca..ec3e1f24 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -924,7 +924,6 @@ let undefined_builtin_val_specs =
    extern_of_string (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}";
    extern_of_string (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
    extern_of_string (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}";
-   (* Only used with lem_mwords *)
    extern_of_string (mk_id "undefined_bitvector") "forall 'n. atom('n) -> bitvector('n, dec) effect {undef}";
    extern_of_string (mk_id "undefined_unit") "unit -> unit effect {undef}"]
 
-- 
cgit v1.2.3