diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-15 12:16:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-16 13:19:52 +0200 |
| commit | 2d4701b4d1bdb0fb4f64dec9ffbd9ad90506ba26 (patch) | |
| tree | 54cf74c1318969da0dcaadf4204aefd840ac4dd2 /checker/values.ml | |
| parent | dcf4d3e28813e09fc71f974b79ddf42d2e525976 (diff) | |
Fixing the checker.
This is a stupid fix that only allows to take into account the change in
memory layout. The check will simply fail when encountering a unguarded
inductive or (co)fixpoint.
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/checker/values.ml b/checker/values.ml index cf56bbd98..5f67b17d3 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 6f563f1f75706b28e5d3e3ef59e1681c checker/cic.mli +MD5 27a5893c01d6f80e7a8741ef98874e63 checker/cic.mli *) @@ -208,6 +208,9 @@ let v_projbody = v_tuple "projection_body" [|v_cst;Int;Int;v_constr;v_tuple "proj_eta" [|v_constr;v_constr|]; v_constr|] +let v_typing_flags = + v_tuple "typing_flags" [|v_bool|] + let v_cb = v_tuple "constant_body" [|v_section_ctxt; v_cst_def; @@ -216,7 +219,8 @@ let v_cb = v_tuple "constant_body" v_bool; v_context; Opt v_projbody; - v_bool|] + v_bool; + v_typing_flags|] let v_recarg = v_sum "recarg" 1 (* Norec *) [|[|v_ind|] (* Mrec *);[|v_ind|] (* Imbr *)|] |