X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Ftypes.ml;h=de7c1036e8cc26ab20e6316e7c157eb7ed95c3c4;hb=137a822662f81efbbeac7ddc833fc9ffe252a70e;hp=73420ee5921d987592cba96ebc646356b50b15f5;hpb=876f16ec4e9080bad4e39bd9c203d6529dcf4f56;p=helm.git

diff --git a/helm/software/components/binaries/transcript/types.ml b/helm/software/components/binaries/transcript/types.ml
index 73420ee59..de7c1036e 100644
--- a/helm/software/components/binaries/transcript/types.ml
+++ b/helm/software/components/binaries/transcript/types.ml
@@ -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