aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/values.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/values.ml')
-rw-r--r--checker/values.ml7
1 files changed, 4 insertions, 3 deletions
diff --git a/checker/values.ml b/checker/values.ml
index 46e1d62c2..86634fbd8 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 c802f941f368bedd96e931cda0559d67 checker/cic.mli
+MD5 62a4037e9e584d508909d631c5e8a759 checker/cic.mli
*)
@@ -54,6 +54,7 @@ let v_enum name n = Sum(name,n,[||])
let v_pair v1 v2 = v_tuple "*" [|v1; v2|]
let v_bool = v_enum "bool" 2
+let v_unit = v_enum "unit" 1
let v_ref v = v_tuple "ref" [|v|]
let v_set v =
@@ -311,13 +312,13 @@ and v_impl =
Sum ("module_impl",2, (* Abstract, FullStruct *)
[|[|v_mexpr|]; (* Algebraic *)
[|v_sign|]|]) (* Struct *)
-and v_noimpl = v_enum "no_impl" 1 (* Abstract is mandatory for mtb *)
+and v_noimpl = v_unit
and v_module =
Tuple ("module_body",
[|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
and v_modtype =
Tuple ("module_type_body",
- [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
+ [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_unit|])
(** kernel/safe_typing *)