diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-21 15:13:07 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-26 14:53:08 +0100 |
| commit | 23a33c1a7781e35faf83ed4c7e42df8c8803e64e (patch) | |
| tree | 02ed94f3bb58df9e58732421b6430ba9d76f4eac /checker/values.ml | |
| parent | 969f56084f2c9eac670e47852518a3ca11fb0174 (diff) | |
fix checker w.r.t. mutual_inductive_body and constant_body
discrepancy introduced in commit d3eac3d5fc8e5af499eb8750ca08ead8562dac6f
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 4 |
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, |