diff options
author | Son HO | 2022-09-22 16:26:00 +0200 |
---|---|---|
committer | GitHub | 2022-09-22 16:26:00 +0200 |
commit | 9dc3b26ecf2bba6993febaca816c6797147ee7b9 (patch) | |
tree | 82815f1137d020cb85040b432955d067f9d9be26 /src | |
parent | ba68c1ab4a7bd7817068d34d44fca38e4c547d90 (diff) |
Update src/TypesUtils.ml
Diffstat (limited to 'src')
-rw-r--r-- | src/TypesUtils.ml | 2 |
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. *) |