X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fbinaries%2Ftranscript%2Ftypes.ml;h=de7c1036e8cc26ab20e6316e7c157eb7ed95c3c4;hb=18238be513728c37e46e637e73476cd98d1bddd5;hp=e51122b3f20e3aaa0788c4af47a123f373f72b0e;hpb=ad17757edcc6cf75be576268fab8cf52751d679a;p=helm.git

diff --git a/components/binaries/transcript/types.ml b/components/binaries/transcript/types.ml
index e51122b3f..de7c1036e 100644
--- a/components/binaries/transcript/types.ml
+++ b/components/binaries/transcript/types.ml
@@ -23,17 +23,24 @@
  * http://cs.unibo.it/helm/.
  *)
 
+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
           | Unexport of string
           | BaseUri of string
 	  | Include of string
-          | Coercion of string
-	  | Notation of string
-	  | Inline of (inline_kind * string)
+          | Coercion of (local * string)
+	  | Notation of (local * string)
+	  | Section of (local * string * string)
+	  | Inline of (local * inline_kind * source * prefix)
           | Verbatim of string
 	  | Discard of string