]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7f398a5) | patch
We have a big architectural problem here: the Hbugs hints when applied
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 2 Apr 2003 11:04:32 +0000 (11:04 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 2 Apr 2003 11:04:32 +0000 (11:04 +0000)
commit34bdae056b1ac678419cc63437f0c92ee58ef228
tree0705de78e5831ad38aebdaddf544898d68ab3886tree | snapshot
parent7f398a57e81555876212ff38c3c0d1cd821b718fcommit | diff
We have a big architectural problem here: the Hbugs hints when applied
may have an argument which is a term (now in textual form). Depending on the
current parser in use, the syntax for the textual form must be TeX or
ASCII art. Which one is the right one? The current momentary patch activates
the TeX syntax.
helm/gTopLevel/hbugs.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.