]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/binaries/transcript/types.ml
matitadep: we now handle the inline of an uri, we removed the -exclude option
[helm.git] / helm / software / components / binaries / transcript / types.ml
index f0c8212bc47c3271c94045d895592f3a785aacbc..2eb25a103c1677a50b2f0b822f9f302c8a8a9fdd 100644 (file)
@@ -37,7 +37,6 @@ type item = Heading of (string * int)
           | Line of string
          | Comment of string
           | Unexport of string
-          | BaseUri of string
          | Include of string
           | Coercion of (local * string)
          | Notation of (local * string)