diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-12-16 10:58:13 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-12-17 17:47:48 +0100 |
| commit | fba1f0ed91aff372234b5a95422ee18f1730522f (patch) | |
| tree | fa5ca22e0af3ad47067c5908385039e1668f7843 /checker/values.ml | |
| parent | f3a6d9080842899e50a44e9474ac0f9a475d5db1 (diff) | |
Update checker/values and cic due to changes in case_info and record_body.
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/checker/values.ml b/checker/values.ml index b38744cc7..f55cf63fc 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -119,9 +119,11 @@ let v_sortfam = v_enum "sorts_family" 3 let v_puniverses v = v_tuple "punivs" [|v;v_instance|] +let v_boollist = List v_bool + let v_caseinfo = let v_cstyle = v_enum "case_style" 5 in - let v_cprint = v_tuple "case_printing" [|Int;v_cstyle|] in + let v_cprint = v_tuple "case_printing" [|v_boollist;Array v_boollist;v_cstyle|] in v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|] let v_cast = v_enum "cast_kind" 4 @@ -251,7 +253,7 @@ let v_one_ind = v_tuple "one_inductive_body" let v_finite = v_enum "recursivity_kind" 3 let v_mind_record = Annot ("mind_record", - Opt (v_tuple "record" [| Array v_cst; Array v_projbody |])) + Opt (Opt (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |]))) let v_ind_pack = v_tuple "mutual_inductive_body" [|Array v_one_ind; |