diff options
Diffstat (limited to 'src/ExtractToFStar.ml')
| -rw-r--r-- | src/ExtractToFStar.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 83eaae9d..506a6d04 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -1011,6 +1011,9 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) (* Open a box for the definition, so that whenever possible it gets printed on * one line - TODO: remove? *) F.pp_open_hvbox fmt 0; + (* Add the `unfold` keyword *) + F.pp_print_string fmt "unfold"; + F.pp_print_space fmt (); (* Open a box for "let FUN_NAME (PARAMS) =" *) F.pp_open_hovbox fmt ctx.indent_incr; (* > "let FUN_NAME" *) |