aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/values.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/values.ml')
-rw-r--r--checker/values.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/checker/values.ml b/checker/values.ml
index b2d74821d..cf56bbd98 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 f5fd749af797e08efee22122742bc740 checker/cic.mli
+MD5 6f563f1f75706b28e5d3e3ef59e1681c checker/cic.mli
*)
@@ -265,7 +265,8 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
v_rctxt;
v_bool;
v_context;
- Opt v_bool|]
+ Opt v_bool;
+ v_bool|]
let v_with =
Sum ("with_declaration_body",0,