diff options
author | Son Ho | 2022-02-01 19:56:38 +0100 |
---|---|---|
committer | Son Ho | 2022-02-01 19:56:38 +0100 |
commit | 5faf86a5718daf2030d77a8e8e1b321ffb13913d (patch) | |
tree | dece421bd8c2d8ee2cf9c7dec715a1de49e18e45 | |
parent | 1416493e000d2eec1541ae7c4077a6c1ae7870c1 (diff) |
Make a minor modification to ExtractToFStar.extract_type_def_enum_body
Diffstat (limited to '')
-rw-r--r-- | src/ExtractToFStar.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index cd6e7962..dcadb773 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -285,6 +285,10 @@ let extract_type_def_enum_body (ctx : extraction_ctx) (fmt : F.formatter) | None -> ctx | Some field_name -> let var_id = VarId.of_int (FieldId.to_int fid) in + let field_name = + ctx.fmt.var_basename ctx.names_map.names_set (Some field_name) + f.field_ty + in let ctx, field_name = ctx_add_var field_name var_id ctx in F.pp_print_string fmt (field_name ^ " :"); F.pp_print_space fmt (); |