Adam Chlipala wrote:
Marc Weber wrote:
The demos make use of it multiple times:
[...]
Or do those ! have a different meaning?
Each of these should be an application of something besides an
identifier defined at the top level of a module.
I should also add that I just realized I left around some obsolete demos
that I haven't tried compiling in probably close to a year. If you want
to examine code that will actually compile, I recommend repeating the
search after pulling the latest version.
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
