diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-25 09:52:45 +0200 |
---|---|---|
committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-25 10:29:08 +0200 |
commit | 28855216037570aeabc544ab232bb896d7a7327f (patch) | |
tree | 0d8d5337c136675581364c86756b7775d56d0061 /checker/values.ml | |
parent | 476189527703aaf9caf5612e8395ce3b8ddb088f (diff) |
Adjust checker after `Assume [Positive]`.
Diffstat (limited to 'checker/values.ml')
-rw-r--r-- | checker/values.ml | 5 |
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, |