From 71863baf896d0f6c07473fce16e7568aa39064bc Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 13 Jan 2023 21:44:26 +0100
Subject: Do not unfold the monadic lets for the generated F* code

---
 compiler/Driver.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index dfe4e908..73a2c974 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -140,8 +140,9 @@ let () =
   let _ =
     match !backend with
     | FStar ->
-        (* F* supports monadic notations, but the encoding loses information *)
-        unfold_monadic_let_bindings := true
+        (* Some patterns are not supported *)
+        decompose_monadic_let_bindings := false;
+        decompose_nested_let_patterns := false
     | Coq ->
         (* Some patterns are not supported *)
         decompose_monadic_let_bindings := true;
-- 
cgit v1.2.3