diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-04-29 09:29:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-04-29 09:43:39 +0200 |
| commit | 3b176883b7fcd9af6881ae1049bbd078c8d19577 (patch) | |
| tree | c73465b8436bb21b26663802fcc70989f3efc885 /checker/values.ml | |
| parent | d9dbff8b8e421406cf76526e39e9504779cbadf0 (diff) | |
Completing 5eb53b5bc8d765ed75e965f43f1084e18efc8790 (I unfortunately
did not notice that kernel/values.ml had to be made consistent with
kernel/cic.mli).
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 b3c070b19..9d2444309 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 c0f79d23d0eb5d2e4cfb53ead514fcf5 checker/cic.mli +MD5 b6df941161847354cea0591850f4d528 checker/cic.mli *) @@ -114,7 +114,7 @@ let v_sortfam = v_enum "sorts_family" 3 let v_caseinfo = let v_cstyle = v_enum "case_style" 5 in let v_cprint = v_tuple "case_printing" [|Int;v_cstyle|] in - v_tuple "case_info" [|v_ind;Int;Array Int;v_cprint|] + v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|] let v_cast = v_enum "cast_kind" 3 (** NB : In fact there are 4 cast markers, but the last one @@ -230,6 +230,7 @@ let v_one_ind = v_tuple "one_inductive_body" List v_sortfam; Array v_constr; Array Int; + Array Int; v_wfp; Int; Int; |