summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon HO2022-09-22 16:26:00 +0200
committerGitHub2022-09-22 16:26:00 +0200
commit9dc3b26ecf2bba6993febaca816c6797147ee7b9 (patch)
tree82815f1137d020cb85040b432955d067f9d9be26
parentba68c1ab4a7bd7817068d34d44fca38e4c547d90 (diff)
Update src/TypesUtils.ml
Diffstat (limited to '')
-rw-r--r--src/TypesUtils.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index 8d0624ee..8088be7f 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -100,7 +100,7 @@ let rty_regions_intersect (ty : rty) (regions : RegionId.Set.t) : bool =
let ty_regions = rty_regions ty in
not (RegionId.Set.disjoint ty_regions regions)
-(** Convert an [ety], containing no region variables, to an [rty] or [sty].
+(** Convert an [ety], containing no region variables, to an [rty] or an [sty].
In practice, it is the identity.
*)