summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-29 21:39:20 +0100
committerSon Ho2022-01-29 21:39:20 +0100
commitc70d13bcd11614833875169f641deb215a0eef1e (patch)
treeab87ee9c6d9c1b5f4977507efcdeadc5e29e5649
parent86dbbf0c02da983123933b89a73f1b2563924d54 (diff)
Make a minor modification
Diffstat (limited to '')
-rw-r--r--src/PureToExtract.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 360ef4a6..a5619eae 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -349,7 +349,7 @@ let ctx_add_type_def (def : type_def) (ctx : extraction_ctx) :
let ctx_add_field (def : type_def) (field_id : FieldId.id) (field : field)
(ctx : extraction_ctx) : extraction_ctx * string =
- let name = ctx.fmt.field_name def.name field.field_name in
+ let name = ctx.fmt.field_name def.name field_id field.field_name in
let ctx = ctx_add (FieldId (def.def_id, field_id)) name ctx in
(ctx, name)