]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0340192) | patch
lexicon commands must tbe parsed before grafite commands rather than
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 26 Jan 2016 16:09:51 +0000 (16:09 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 26 Jan 2016 16:09:51 +0000 (16:09 +0000)
commit7d8ebeb7b6f21204b88786c738c67f52f3703c5b
tree94a0bcea05b7307707aa1c3ef8b15de358cc27fdtree | snapshot
parent03401922e645207c7b64b52e1c4349f7951fcf71commit | diff
lexicon commands must tbe parsed before grafite commands rather than
after (why?)
matita/components/grafite_parser/grafiteParser.ml diff | blob | history
matita/matita/.depend.opt diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.