]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/binaries/transcript/engine.ml
bug fix in inline syntax
[helm.git] / helm / software / components / binaries / transcript / engine.ml
index f4b0c1e3747c4b616ca7e4ad6b3b45aaaa411dbb..8009483f14028221e4786531f3b9affaf5debb1c 100644 (file)
@@ -189,13 +189,13 @@ let produce st =
       let in_base_uri = Filename.concat st.input_base_uri name in
       let out_base_uri = Filename.concat st.output_base_uri name in
       let filter path = function
-         | T.Inline (b, k, obj, p)      -> 
+         | T.Inline (b, k, obj, p, f)   -> 
            let obj, p = 
               if b then Filename.concat (make_path path) obj, make_prefix path
               else obj, p
            in 
            let s = obj ^ G.string_of_inline_kind k in
-           path, Some (T.Inline (b, k, Filename.concat in_base_uri s, p))
+           path, Some (T.Inline (b, k, Filename.concat in_base_uri s, p, f))
         | T.Include s                  ->
            begin 
               try path, Some (T.Include (List.assoc s st.requires))