X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=examples%2FRegexMatcher.hs;h=a50a10bca419955abe2efcc7b013678267a8b569;hp=ca0275559819fbf0b5d88275d46c53c1068b373b;hb=b096aab78240e38ff69c120367e65be60cbc54f5;hpb=caa7ad74b99b34abc5181553e66423da6bdfee26

diff --git a/examples/RegexMatcher.hs b/examples/RegexMatcher.hs
index ca02755..a50a10b 100644
--- a/examples/RegexMatcher.hs
+++ b/examples/RegexMatcher.hs
@@ -110,13 +110,12 @@ staged_accept (Times e1 e2) emptyOk k    =
 staged_accept (Star e) emptyOk' k  =
    loop emptyOk'
     where
-    -- loop :: Bool -> <[s -> Bool]>@g
+     -- Note that the type of "loop" is NOT (forall c s. <[s -> Bool]>@c)
+     -- because "k" is free here; this restrictionis analogous to the free
+     -- environment variable in Nanevski's example.  
      loop emptyOk = if emptyOk
                     then <[ \s -> ~~k s || ~~(staged_accept e True  (loop False)) s ]>
                     else <[ \s ->          ~~(staged_accept e False (loop False)) s ]>
-    -- note that loop is not (forall c s. <[s -> Bool]>@c)
-    -- because "k" is free in loop; it is analogous to the free
-    -- environment variable in Nanevski's example
 
 staged_accept (Const c) emptyOk k  =
     <[ \s -> if gs_empty s