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

diff --git a/helm/software/components/binaries/transcript/types.ml b/helm/software/components/binaries/transcript/types.ml
index d7770ade7..fbe112a83 100644
--- a/helm/software/components/binaries/transcript/types.ml
+++ b/helm/software/components/binaries/transcript/types.ml
@@ -23,16 +23,27 @@
  * http://cs.unibo.it/helm/.
  *)
 
+type local = bool
+
 type inline_kind = Con | Ind | Var
 
+type output_kind = Declarative | Procedural
+
+type source = string
+
+type prefix = string
+
+type flavour = Cic.object_flavour option
+
 type item = Heading of (string * int)
-          | Comment of string
+          | 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 * flavour)
           | Verbatim of string
 	  | Discard of string