]> matita.cs.unibo.it Git - helm.git/blobdiff - components/binaries/transcript/types.ml
rc-1
[helm.git] / components / binaries / transcript / types.ml
index 73420ee5921d987592cba96ebc646356b50b15f5..de7c1036e8cc26ab20e6316e7c157eb7ed95c3c4 100644 (file)
@@ -27,6 +27,10 @@ type local = bool
 
 type inline_kind = Con | Ind | Var
 
+type source = string
+
+type prefix = string
+
 type item = Heading of (string * int)
           | Line of string
          | Comment of string
@@ -35,7 +39,8 @@ type item = Heading of (string * int)
          | Include of string
           | Coercion of (local * string)
          | Notation of (local * string)
-         | Inline of (inline_kind * string)
+         | Section of (local * string * string)
+         | Inline of (local * inline_kind * source * prefix)
           | Verbatim of string
          | Discard of string