]> matita.cs.unibo.it Git - helm.git/blobdiff - components/binaries/transcript/engine.ml
Big progress
[helm.git] / components / binaries / transcript / engine.ml
index 9824426daf5497dceb4c62ec5590b3323a65cf1c..66c6c33be85a2b53e16352a7c41b57e77ee2a8d0 100644 (file)
@@ -186,10 +186,8 @@ let produce st =
            end
         | T.Coercion (b, obj)          ->
            let str = get_coercion st obj in
-           let base_uri = 
-              if str <> "" then str else 
-              if b then out_base_uri else in_base_uri
-           in
+           if str <> "" then path, Some (T.Coercion (b, str)) else
+           let base_uri = if b then out_base_uri else in_base_uri in
            let s = obj ^ G.string_of_inline_kind T.Con in
            path, Some (T.Coercion (b, Filename.concat base_uri s))
         | T.Section (b, id, _) as item ->
@@ -215,6 +213,6 @@ let produce st =
       with e -> 
          prerr_endline (Printexc.to_string e); close_in ich 
    in
-   init st.input_package; 
+   init st.input_package; require st st.input_package "preamble"; 
    List.iter (produce st) st.files; 
    commit st st.input_package