diff options
| author | JPR | 2019-05-22 21:40:57 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-23 01:49:04 +0200 |
| commit | 467eb67bb960c15e1335f375af29b4121ac5262b (patch) | |
| tree | 1ad2454c535b090738748cd8123330451a498854 /kernel/inductive.ml | |
| parent | 20a464396fd89449569dc69b8cfb37cb69766733 (diff) | |
Fixing typos - Part 2
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 *) |