diff options
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/checker/values.ml b/checker/values.ml index 67032bd1b..f1c4fd470 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 fb80632357e3ffa988c6bba3fa6ade64 checker/cic.mli +MD5 3d9612f0adc70404fddb093b85c7d168 checker/cic.mli *) @@ -241,7 +241,6 @@ let v_cb = v_tuple "constant_body" Any; v_const_univs; v_bool; - v_bool; v_typing_flags|] let v_recarg = v_sum "recarg" 1 (* Norec *) |