aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--checker/values.ml4
1 files changed, 1 insertions, 3 deletions
diff --git a/checker/values.ml b/checker/values.ml
index 9a0d9922f..95befa287 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,