summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Driver.ml5
1 files changed, 3 insertions, 2 deletions
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;