summaryrefslogtreecommitdiff
path: root/src/Pure.ml
diff options
context:
space:
mode:
authorSon Ho2022-02-03 13:53:02 +0100
committerSon Ho2022-02-03 13:53:02 +0100
commit76bb70b3f6dc9240d7ffa121a66be489c751add6 (patch)
tree85515ba05b67454c1c7de7865a1c699d56b6bb03 /src/Pure.ml
parent972ed4288ff1f489fcf03b4cdca847abcc55674e (diff)
Implement ExtractToFStar.extract_typed_rvalue
Diffstat (limited to '')
-rw-r--r--src/Pure.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Pure.ml b/src/Pure.ml
index 32a1ca4c..fd3eb03f 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -134,6 +134,9 @@ type var = {
itself.
*)
+(* TODO: we might want to redefine field_proj_kind here, to prevent field accesses
+ * on enumerations.
+ * Also: tuples... *)
type projection_elem = { pkind : E.field_proj_kind; field_id : FieldId.id }
type projection = projection_elem list