From 34fed5feb6b768cdf1489936cc1529898bdcc4e9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 22 Sep 2022 18:32:03 +0200
Subject: Add some comments

---
 src/ExtractToFStar.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src/ExtractToFStar.ml')

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,
-- 
cgit v1.2.3