diff options
| -rw-r--r-- | kernel/inductive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 3e2f03871a..545b5b83a1 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -416,7 +416,7 @@ let inductive_of_fix env recarg body = subterm_specif env c ind subterm_specif should test if [c] (building objects of inductive - type [ind], not necassarily the same as that of the recursive + type [ind], not necessarily the same as that of the recursive argument) is a subterm of the recursive argument of the fixpoint we are checking and fails with Not_found if not. In case it is, it should send its recursive specification (i.e. on which arguments we |