From: Ferruccio Guidi Date: Sun, 10 Mar 2013 12:01:43 +0000 (+0000) Subject: we removed a useless assertion that was forcing matita to edit just matita files X-Git-Tag: make_still_working~1226 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eab4837fe057c5b90b2484b7257d115627db6d6f;p=helm.git 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! --- diff --git a/matita/components/library/librarian.ml b/matita/components/library/librarian.ml index 9ffde2b87..13fccbfa2 100644 --- a/matita/components/library/librarian.ml +++ b/matita/components/library/librarian.ml @@ -111,8 +111,12 @@ let find_root_for ~include_paths file = let mk_baseuri root extra = let chop name = +(* FG: there is no reason why matita should edit just matita files + matita's editor is good on its own and has interesting facilities + including predefined virtuals assert(Filename.check_suffix name ".ma" || Filename.check_suffix name ".mma"); +*) try Filename.chop_extension name with Invalid_argument "Filename.chop_extension" -> name in