diff options
Diffstat (limited to 'checker/term.mli')
| -rw-r--r-- | checker/term.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/term.mli b/checker/term.mli index 1367e5813..66ba96cc5 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -12,7 +12,7 @@ type case_printing = { ind_nargs : int; style : case_style; } type case_info = { ci_ind : inductive; ci_npar : int; - ci_cstr_nargs : int array; + ci_cstr_ndecls : int array; ci_pp_info : case_printing; } type contents = Pos | Null |