Add some comments

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,