From 3b176883b7fcd9af6881ae1049bbd078c8d19577 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 29 Apr 2014 09:29:27 +0200
Subject: Completing 5eb53b5bc8d765ed75e965f43f1084e18efc8790 (I unfortunately
 did not notice that kernel/values.ml had to be made consistent with
 kernel/cic.mli).

---
 checker/values.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/checker/values.ml b/checker/values.ml
index b3c070b19b..9d2444309a 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;
-- 
cgit v1.2.3