]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (from: 34bdae0)
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)
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.


No differences found
Unnamed repository; edit this file 'description' to name the repository.