diff options
Diffstat (limited to 'typing/subst.mli')
| -rw-r--r-- | typing/subst.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/typing/subst.mli b/typing/subst.mli index 55eee757d7..b92f338d4c 100644 --- a/typing/subst.mli +++ b/typing/subst.mli @@ -21,9 +21,9 @@ type t (* Substitutions are used to translate a type from one context to - another. This requires substituing paths for identifiers, and + another. This requires substituting paths for identifiers, and possibly also lowering the level of non-generic variables so that - it be inferior to the maximum level of the new context. + they are inferior to the maximum level of the new context. Substitutions can also be used to create a "clean" copy of a type. Indeed, non-variable node of a type are duplicated, with their |