diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-12 21:41:03 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-31 10:13:33 +0200 |
commit | c7bd285555153294ec077cfa05c36bb420716f3b (patch) | |
tree | e6f414e1f0e5914a17c98e104d49691bae27035b /checker/values.ml | |
parent | 4598a26890a896ddcf6cd30758ae07882e245a16 (diff) |
Reduce circular dependency constants <-> projections
Instead of having the projection data in the constant data we have it
independently in the environment.
Diffstat (limited to 'checker/values.ml')
-rw-r--r-- | checker/values.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/values.ml b/checker/values.ml index 1ac8d7cef..f7ab95fe2 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 c4fdf8a846aed45c27b5acb1add7d1c6 checker/cic.mli +MD5 92de14d7bf9134532e8a0cff5618bd50 checker/cic.mli *) @@ -240,7 +240,7 @@ let v_cb = v_tuple "constant_body" v_constr; Any; v_const_univs; - Opt v_projbody; + v_bool; v_bool; v_typing_flags|] |