aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/values.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/values.ml')
-rw-r--r--checker/values.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/values.ml b/checker/values.ml
index 12fbf1ff0..45f04f88d 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 125f04aeb55b2fa027db6bfb9dffc6a2 checker/cic.mli
+MD5 07651f61f86d91b22ff7056c6a8d86bc checker/cic.mli
*)
@@ -225,7 +225,7 @@ let v_cst_def =
let v_projbody =
v_tuple "projection_body"
- [|v_cst;Int;Int;v_constr;v_constr|]
+ [|v_cst;Int;Int;v_constr|]
let v_typing_flags =
v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]