diff options
Diffstat (limited to 'kernel/inductive.ml')
| -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 d9335d39b5..ca7086a3e4 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -166,7 +166,7 @@ let make_subst env = (* template, it is identity substitution otherwise (ie. when u is *) (* already in the domain of the substitution) [remember_subst] will *) (* update its image [x] by [sup x u] in order not to forget the *) - (* dependency in [u] that remains to be fullfilled. *) + (* dependency in [u] that remains to be fulfilled. *) make (remember_subst u subst) (sign, exp, []) | _sign, [], _ -> (* Uniform parameters are exhausted *) |