summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-02-03 23:30:49 +0100
committerSon Ho2022-02-03 23:30:49 +0100
commit0c9743cbce77e473bb7941230f9222f6dd768dfa (patch)
tree1e3d3e280ff84d08e5417eb63ebe086a732fc349
parent1b8b473bb3325713b72e12c7adfba3e024fdf194 (diff)
Make a minor modification
-rw-r--r--src/ExtractToFStar.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 7d8e84c4..8f68ed84 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -710,7 +710,6 @@ 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