diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 9a59a889b4..16c6b6c773 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -64,7 +64,6 @@ type constructor_summary = { (* A light version of mind_specif_of_mind with pre-splitted args *) (* and a receipt to build a summary of constructors *) type inductive_summary = { - fullmind : constr; mind : inductive; params : constr list; realargs : constr list; |