From 2a0ecfbef81231a394df71817a4cd9e81582b7de Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 13 Nov 2022 23:02:00 +0100
Subject: Make minor modifications

---
 compiler/ExtractToCoq.ml        | 8 --------
 compiler/ExtractToFStar.ml      | 8 --------
 compiler/dune                   | 2 --
 tests/coq/misc/External__Funs.v | 3 +--
 4 files changed, 1 insertion(+), 20 deletions(-)
 delete mode 100644 compiler/ExtractToCoq.ml
 delete mode 100644 compiler/ExtractToFStar.ml

diff --git a/compiler/ExtractToCoq.ml b/compiler/ExtractToCoq.ml
deleted file mode 100644
index 3681adc3..00000000
--- a/compiler/ExtractToCoq.ml
+++ /dev/null
@@ -1,8 +0,0 @@
-(** Utilities for the extraction to Coq *)
-
-open Utils
-open Pure
-open TranslateCore
-open ExtractBase
-open StringUtils
-module F = Format
diff --git a/compiler/ExtractToFStar.ml b/compiler/ExtractToFStar.ml
deleted file mode 100644
index 21a6fc8f..00000000
--- a/compiler/ExtractToFStar.ml
+++ /dev/null
@@ -1,8 +0,0 @@
-(** Utilities for the extraction to F* *)
-
-open Utils
-open Pure
-open TranslateCore
-open ExtractBase
-open StringUtils
-module F = Format
diff --git a/compiler/dune b/compiler/dune
index b530340b..b825ef7e 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -22,8 +22,6 @@
   ExpressionsUtils
   Extract
   ExtractBase
-  ExtractToCoq
-  ExtractToFStar
   FunsAnalysis
   Identifiers
   InterpreterBorrowsCore
diff --git a/tests/coq/misc/External__Funs.v b/tests/coq/misc/External__Funs.v
index 77b738b0..df35f7eb 100644
--- a/tests/coq/misc/External__Funs.v
+++ b/tests/coq/misc/External__Funs.v
@@ -84,8 +84,7 @@ Definition test_custom_swap_back
   result (state * (u32 * u32))
   :=
   p <- custom_swap_back u32 x y st (1 %u32) st0;
-  let (st1, tmp) := p in
-  let (x0, y0) := tmp in Return (st1, (x0, y0))
+  let (st1, (x0, y0)) := p in Return (st1, (x0, y0))
   .
 
 (** [external::test_swap_non_zero] *)
-- 
cgit v1.2.3