summaryrefslogtreecommitdiff
path: root/src/Pure.ml
diff options
context:
space:
mode:
authorSon Ho2022-04-20 14:05:31 +0200
committerSon Ho2022-04-20 14:05:31 +0200
commitdfabb15cf7bd216e3abffd8df451da1ba36e7b8a (patch)
tree3d8e528a84b5b9559f6542e2d994b7e5e798bfb2 /src/Pure.ml
parent3f173a5ec9425e5b931684cc5143edae21533caa (diff)
Improve the generation of pretty names by correctly using the
left constraints
Diffstat (limited to 'src/Pure.ml')
-rw-r--r--src/Pure.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Pure.ml b/src/Pure.ml
index 9efab912..58ee0b98 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -236,7 +236,7 @@ class virtual ['self] mapreduce_value_base =
end
type var_or_dummy =
- | Var of var * mplace option
+ | Var of var * mplace option (* TODO: the mplace is actually always a variable *)
| Dummy (** Ignored value: `_`. *)
[@@deriving
show,