X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Ftypes.ml;h=fbe112a83616ae7709c16727fb4757772bec1178;hb=347a92a83c3fa154c850d94b1a211fbb8334d4f1;hp=2eb25a103c1677a50b2f0b822f9f302c8a8a9fdd;hpb=32e77480c65cbf23ae7dea38a519c83dfeaf3830;p=helm.git

diff --git a/helm/software/components/binaries/transcript/types.ml b/helm/software/components/binaries/transcript/types.ml
index 2eb25a103..fbe112a83 100644
--- a/helm/software/components/binaries/transcript/types.ml
+++ b/helm/software/components/binaries/transcript/types.ml
@@ -33,6 +33,8 @@ type source = string
 
 type prefix = string
 
+type flavour = Cic.object_flavour option
+
 type item = Heading of (string * int)
           | Line of string
 	  | Comment of string
@@ -41,7 +43,7 @@ type item = Heading of (string * int)
           | Coercion of (local * string)
 	  | Notation of (local * string)
 	  | Section of (local * string * string)
-	  | Inline of (local * inline_kind * source * prefix)
+	  | Inline of (local * inline_kind * source * prefix * flavour)
           | Verbatim of string
 	  | Discard of string