diff options
| author | Son Ho | 2022-02-03 23:30:49 +0100 |
|---|---|---|
| committer | Son Ho | 2022-02-03 23:30:49 +0100 |
| commit | 0c9743cbce77e473bb7941230f9222f6dd768dfa (patch) | |
| tree | 1e3d3e280ff84d08e5417eb63ebe086a732fc349 | |
| parent | 1b8b473bb3325713b72e12c7adfba3e024fdf194 (diff) | |
Make a minor modification
| -rw-r--r-- | src/ExtractToFStar.ml | 1 |
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 |