summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--backend/CastOptim.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/CastOptim.v b/backend/CastOptim.v
index 3ae5ab0..545564d 100644
--- a/backend/CastOptim.v
+++ b/backend/CastOptim.v
@@ -32,11 +32,11 @@ Require Import Kildall.
Inductive approx : Type :=
| Unknown (**r any value *)
| Int7 (**r [[0,127]] *)
- | Int8s (**r [[-128,127] *)
+ | Int8s (**r [[-128,127]] *)
| Int8u (**r [[0,255]] *)
| Int15 (**r [[0,32767]] *)
| Int16s (**r [[-32768,32767]] *)
- | Int16u (**r [[0,65535] *)
+ | Int16u (**r [[0,65535]] *)
| Single (**r single-precision float *)
| Novalue. (**r empty *)