]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/binaries/xoa/xoa.ml
- xoa: the definitions file now includes the notations file
[helm.git] / matita / components / binaries / xoa / xoa.ml
index ae5bd03abc9c8da298f39e89c9af86da4880bbef..e4e0e7c69f17bcbca0b0b6dd7b19f0d6711c6d46 100644 (file)
@@ -32,6 +32,7 @@ let process conf =
       let ooch = L.open_out preamble (R.get_string "xoa.objects") in
       let noch = L.open_out preamble (R.get_string "xoa.notations") in
       List.iter (L.out_include ooch) (R.get_list R.string "xoa.include");   
+      L.out_include ooch (R.get_string "xoa.notations" ^ ".ma");      
       List.iter (E.generate ooch noch) (R.get_list unm_ex "xoa.ex");
       List.iter (E.generate ooch noch) (R.get_list unm_or "xoa.or");
       List.iter (E.generate ooch noch) (R.get_list unm_and "xoa.and");