summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-22 21:55:33 +0100
committerSon Ho2021-11-22 21:55:33 +0100
commit01c932290477381c55745801e2545bed759ad77b (patch)
tree9ada41b52d6d36d0d6cf40531c32737a0312feea
parent5dd233cf1ed8fad120f79f6e002d15607b520cc9 (diff)
Add a comment
Diffstat (limited to '')
-rw-r--r--src/Expressions.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Expressions.ml b/src/Expressions.ml
index c0ee90a9..0246530b 100644
--- a/src/Expressions.ml
+++ b/src/Expressions.ml
@@ -4,6 +4,7 @@ open Values
type field_proj_kind =
| ProjAdt of TypeDefId.id * VariantId.id option
| ProjTuple of int
+(* arity of the tuple *)
type projection_elem =
| Deref