diff options
Diffstat (limited to 'kernel/indtypes.mli')
| -rw-r--r-- | kernel/indtypes.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 7e803b11e..532471ebc 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -52,7 +52,6 @@ then, in $i^{th}$ block, [mind_entry_params] is [[xn:Xn;...;x1:X1]]; *) type one_inductive_entry = { - mind_entry_nparams : int; mind_entry_params : (identifier * local_entry) list; mind_entry_typename : identifier; mind_entry_arity : constr; |