From 6a6134dbcb8039a74f38c7cdc8af63cd3b320c61 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Feb 2022 21:06:11 +0100
Subject: Implement a micro pass to filter the box functions

---
 src/ExtractToFStar.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/ExtractToFStar.ml')

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 2994d95f..a3972578 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -692,6 +692,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
       let _ = extract_typed_rvalue ctx fmt inside rv in
       ()
   | Call call -> (
+      log#ldebug (lazy ("ctx_get_function: " ^ show_fun_id call.func));
       match (call.func, call.args) with
       | Unop unop, [ arg ] ->
           ctx.fmt.extract_unop (extract_texpression ctx fmt) fmt inside unop arg
-- 
cgit v1.2.3