]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: add1600) | patch
we removed a useless assertion that was forcing matita to edit just matita files
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 10 Mar 2013 12:01:43 +0000 (12:01 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 10 Mar 2013 12:01:43 +0000 (12:01 +0000)
commiteab4837fe057c5b90b2484b7257d115627db6d6f
treec3ec91cdc0ea5f71efade278029c5c911670c50dtree | snapshot
parentadd1600e1ceef0f1c7e07a4d13c60edd7a3ea367commit | diff
we removed a useless assertion that was forcing matita to edit just matita files
matita's editor is good on its own and has interesting facilities including predefined virtuals
in lambdadelta we use matita to edit the .tbl files containing notation from the .ma's
and we use matita as well to edit predefined_virtuals.ml
we still wonder how we could do this up to now despite the assertion!
matita/components/library/librarian.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.