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 9ffde2b87d0444c6d9ad012b4e26e9641d45a513..13fccbfa25479beee0e52634cc75ebddf7dbf2ec 100644 (file)
--- 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