From 23a33c1a7781e35faf83ed4c7e42df8c8803e64e Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 21 Feb 2014 15:13:07 +0100
Subject: fix checker w.r.t. mutual_inductive_body and constant_body

discrepancy introduced in commit d3eac3d5fc8e5af499eb8750ca08ead8562dac6f
---
 checker/values.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/checker/values.ml b/checker/values.ml
index 9a0d9922f9..95befa2870 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -199,7 +199,6 @@ let v_cb = v_tuple "constant_body"
     v_cst_type;
     Any;
     v_computation v_cstrs;
-    Any;
     v_bool|]
 
 let v_recarg = v_sum "recarg" 1 (* Norec *)
@@ -242,8 +241,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     Int;
     Int;
     v_rctxt;
-    v_cstrs;
-    Any|]
+    v_cstrs|]
 
 let v_with =
   Sum ("with_declaration_body",0,
-- 
cgit v1.2.3