From 2e91b90e332c473253c2ff91fd65da34eb709572 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 11 Jun 2024 14:06:23 +0200
Subject: Deactivate the use of tuple projectors in the Lean backend

---
 compiler/SymbolicToPure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 3975107a..87f1128d 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2916,7 +2916,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
            at once (`let (a, b, c) = x in`) *)
         || TypesUtils.type_decl_from_type_id_is_tuple_struct
              ctx.type_ctx.type_infos type_id
-           && not (Config.backend_has_tuple_projectors ())
+           && not !Config.use_tuple_projectors
       in
       if use_let_with_cons then
         (* Introduce a let binding which expands the ADT *)
-- 
cgit v1.2.3