0. core_notation.ma splitted into coq.moo and core_notation.moo

[helm.git] / helm / matita / matitaMisc.ml

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index ca8dc2446660ec11d5e424119f53be2ff4ebd6a4..e3aadd5b5a616d143c17dd22ab71d25f7ac06626 100644 (file)
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -291,8 +291,9 @@ let obj_file_of_baseuri baseuri =
   path ^ ".moo"
 
 let obj_file_of_script f =
- let baseuri = baseuri_of_file f in
-  obj_file_of_baseuri baseuri
+ if f = "coq.ma" then BuildTimeConf.coq_notation_script else
+  let baseuri = baseuri_of_file f in
+   obj_file_of_baseuri baseuri
 
 let rec list_uniq = function 
   | [] -> []