From 0f736fcb7fd46d902dffa171d1458253b2070b79 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Wed, 6 Feb 2019 03:20:03 +0000
Subject: Remove all sizeof rewriting from C compilation

All sizeof expressions now removed by the type-checker, so it's now
properly a type error if they cannot be removed rather than a bizarre
re-write error. This also greatly improves compilation speed overall, at
the expense of the first type-checking pass.
---
 lib/smt.sail | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/smt.sail b/lib/smt.sail
index e73897b1..6a5a1327 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -19,7 +19,7 @@ val mod = {
   lem: "integerMod",
   c: "tmod_int",
   coq: "emod_with_eq"
-} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == mod('n, 'm). atom('o)}
+} : forall 'n 'm. (atom('n), atom('m)) -> atom(mod('n, 'm))
 
 overload operator % = {mod}
 
@@ -29,7 +29,7 @@ val abs_atom = {
   lem: "abs_int",
   c: "abs_int",
   coq: "abs_with_eq"
-} : forall 'n. atom('n) -> {'o, 'o == abs_atom('n). atom('o)}
+} : forall 'n. atom('n) -> atom(abs('n))
 
 $ifdef TEST
 
-- 
cgit v1.2.3