]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/library/librarian.ml
Keeping track of locations of disambiguated ids and symbols.
[helm.git] / matitaB / components / library / librarian.ml
index 9ffde2b87d0444c6d9ad012b4e26e9641d45a513..899a9a6a5b4f040a675b46ecc5a7b61813f9c5fa 100644 (file)
@@ -112,7 +112,8 @@ let find_root_for ~include_paths file =
 let mk_baseuri root extra =
   let chop name = 
     assert(Filename.check_suffix name ".ma" ||
-      Filename.check_suffix name ".mma");
+      Filename.check_suffix name ".mma" ||
+      Filename.check_suffix name ".mad");
     try Filename.chop_extension name
     with Invalid_argument "Filename.chop_extension" -> name
   in