aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/values.ml
diff options
context:
space:
mode:
authorGravatar Arnaud Spiwack <arnaud@spiwack.net>2015-06-25 09:52:45 +0200
committerGravatar Arnaud Spiwack <arnaud@spiwack.net>2015-06-25 10:29:08 +0200
commit28855216037570aeabc544ab232bb896d7a7327f (patch)
tree0d8d5337c136675581364c86756b7775d56d0061 /checker/values.ml
parent476189527703aaf9caf5612e8395ce3b8ddb088f (diff)
Adjust checker after `Assume [Positive]`.
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,