From a52939b5119e2751570582533bf27828724c2e9f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 23 Dec 2023 01:18:37 +0100
Subject: Fix an issue when deconstructing tuples in Coq

---
 compiler/Extract.ml | 10 ++++++++--
 compiler/Main.ml    |  3 ---
 2 files changed, 8 insertions(+), 5 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 30b76ceb..87dcb1fd 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -132,9 +132,15 @@ let extract_adt_g_value
       F.pp_print_string fmt "tt";
       ctx)
     else
-      (* If there is exactly one value, we don't print the parentheses *)
+      (* If there is exactly one value, we don't print the parentheses.
+         Also, for Coq, we need the special syntax ['(...)] if we destruct
+         a tuple pattern in a let-binding and the tuple has > 2 values.
+      *)
       let lb, rb =
-        if List.length field_values = 1 then ("", "") else ("(", ")")
+        if List.length field_values = 1 then ("", "")
+        else if !backend = Coq && is_single_pat && List.length field_values > 2
+        then ("'(", ")")
+        else ("(", ")")
       in
       F.pp_print_string fmt lb;
       let ctx =
diff --git a/compiler/Main.ml b/compiler/Main.ml
index abc27b46..0b8ec439 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -196,9 +196,6 @@ let () =
   let _ =
     match !backend with
     | FStar ->
-        (* Some patterns are not supported *)
-        decompose_monadic_let_bindings := false;
-        decompose_nested_let_patterns := false;
         (* F* can disambiguate the field names *)
         record_fields_short_names := true
     | Coq ->
-- 
cgit v1.2.3