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 ec0f88a4..b537e181 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -914,6 +914,9 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) | Switch (scrut, body) -> extract_Switch ctx fmt inside scrut body | Meta (_, e) -> extract_texpression ctx fmt inside e +(* Extract an application *or* a top-level qualif (function extraction has + * to handle top-level qualifiers, so it seemed more natural to merge the + * two cases) *) and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (app : texpression) (args : texpression list) : unit = (* We don't do the same thing if the app is a top-level identifier (function, |