From 6f37e6b72905eff8f2c7078823e5577bc5b55eb0 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 24 May 2020 20:44:12 +0200
Subject: small comment

---
 spartan/lib/lib.ML | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'spartan/lib')

diff --git a/spartan/lib/lib.ML b/spartan/lib/lib.ML
index fd5c597..615f601 100644
--- a/spartan/lib/lib.ML
+++ b/spartan/lib/lib.ML
@@ -78,6 +78,8 @@ val type_of_typing = #2 o dest_typing
 fun mk_Pi v typ body = Const (\<^const_name>\<open>Pi\<close>, dummyT) $ typ $ lambda v body
 
 fun typing_of_term tm = \<^const>\<open>has_type\<close> $ tm $ Var (("*?", 0), \<^typ>\<open>o\<close>)
+(*The above is a bit hacky; basically we need to guarantee that the schematic
+  var is fresh*)
 
 
 (** Goals **)
-- 
cgit v1.2.3