From f2ea90c5a9e4a50f90448dea71ee2489029501c5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 8 Mar 2023 00:45:15 +0100
Subject: Make a minor fix

---
 compiler/Extract.ml | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 476359f0..f3061273 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2061,13 +2061,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
     let var_name = ctx_get_var (Option.get supd.init) ctx in
     F.pp_print_string fmt var_name;
     F.pp_print_space fmt ();
-    let where_keyword =
-      match !backend with
-      | FStar -> "where"
-      | Lean -> "with"
-      | Coq -> raise (Failure "Unreachable")
-    in
-    F.pp_print_string fmt where_keyword;
+    F.pp_print_string fmt "with";
     F.pp_print_space fmt ());
   F.pp_open_hvbox fmt 0;
   let delimiter = match !backend with Lean -> "," | Coq | FStar -> ";" in
-- 
cgit v1.2.3