summaryrefslogtreecommitdiff
path: root/typing/subst.mli
diff options
context:
space:
mode:
authorFourchaux <jprodi04@gmail.com>2017-08-10 12:59:23 +0200
committerMark Shinwell <mshinwell@gmail.com>2017-08-10 11:59:23 +0100
commit72cfdd56e9459af07731451c4c10ae0ec2c6d877 (patch)
treeb1958e44ee1ea40bcca88e4a2445ce42f878e724 /typing/subst.mli
parent9a1ddfa2dac2207b3a75a32bf9550fb4bcb39f6e (diff)
downloadocaml-72cfdd56e9459af07731451c4c10ae0ec2c6d877.tar.gz
Typos and basic grammar error fixing (#1280)
Diffstat (limited to 'typing/subst.mli')
-rw-r--r--typing/subst.mli4
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