X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Ftypes.ml;h=1fa7971b761bdccb0596eb6b27d973add38a3993;hb=d17a38ddca548c784e9efa7c55e87c80203b024d;hp=7b17db7b202342c5fa218906d48e7ef7f6252640;hpb=3bfc56cd9b5afe52c3abfbef886ce82efa3bb3a3;p=helm.git

diff --git a/helm/software/components/binaries/transcript/types.ml b/helm/software/components/binaries/transcript/types.ml
index 7b17db7b2..1fa7971b7 100644
--- a/helm/software/components/binaries/transcript/types.ml
+++ b/helm/software/components/binaries/transcript/types.ml
@@ -27,7 +27,7 @@ type local = bool
 
 type inline_kind = Con | Ind | Var
 
-type input_kind = Gallina8 | Grafite
+type input_kind = Gallina8 | Grafite of string
 
 type output_kind = Declarative | Procedural
 
@@ -37,15 +37,17 @@ type prefix = string
 
 type flavour = Cic.object_flavour option
 
+type params = GrafiteAst.inline_param list
+
 type item = Heading of (string * int)
           | Line of string
 	  | Comment of string
           | Unexport of string
-	  | Include of string
+	  | Include of (bool * string)
           | Coercion of (local * string)
 	  | Notation of (local * string)
 	  | Section of (local * string * string)
-	  | Inline of (local * inline_kind * source * prefix * flavour)
+	  | Inline of (local * inline_kind * source * prefix * flavour * params)
           | Verbatim of string
 	  | Discard of string