From 931fabe3e8590815548d606b33fc8db31e9f6010 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Aug 2023 16:21:43 +0200
Subject: Fix an issue with the extraction of aggregated arrays

---
 compiler/PureMicroPasses.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'compiler/PureMicroPasses.ml')

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 00620c58..58a5f9e2 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -611,7 +611,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     (!Config.backend <> Lean && !Config.backend <> Coq)
                     || not is_rec
                   then
-                    let struct_id = adt_id in
+                    let struct_id = AdtId adt_id in
                     let init = None in
                     let updates =
                       FieldId.mapi
@@ -1168,8 +1168,8 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                       Var v ) ->
                       (* We check that this is the proper ADT, and the proper field *)
                       if
-                        proj_adt_id = struct_id && field_id = fid
-                        && x.ty = adt_ty
+                        AdtId proj_adt_id = struct_id
+                        && field_id = fid && x.ty = adt_ty
                       then Some v
                       else None
                   | _ -> None)
-- 
cgit v1.2.3