]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/binaries/transcript/types.ml
- hExtlib: new function "list_assoc_all"
[helm.git] / helm / software / components / binaries / transcript / types.ml
index 3b774f8324fae1c58bebb7fd575b42e5578fe0ac..28641d3d3d82b856512f022a1b337ab6a97eafe8 100644 (file)
@@ -37,6 +37,8 @@ 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
@@ -45,7 +47,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 * flavour)
+         | Inline of (local * inline_kind * source * prefix * flavour * params)
           | Verbatim of string
          | Discard of string