New functorialization: paramod is abstracted over a Orderings.Blob, that is like...

[helm.git] / helm / software / components / binaries / transcript / types.ml

diff --git a/helm/software/components/binaries/transcript/types.ml b/helm/software/components/binaries/transcript/types.ml
index de7c1036e8cc26ab20e6316e7c157eb7ed95c3c4..1fa7971b761bdccb0596eb6b27d973add38a3993 100644 (file)
--- a/helm/software/components/binaries/transcript/types.ml
+++ b/helm/software/components/binaries/transcript/types.ml
@@ -27,20 +27,27 @@ type local = bool
 
 type inline_kind = Con | Ind | Var
 
+type input_kind = Gallina8 | Grafite of string
+
+type output_kind = Declarative | Procedural
+
 type source = string
 
 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
-          | BaseUri 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)
+         | Inline of (local * inline_kind * source * prefix * flavour * params)
           | Verbatim of string
          | Discard of string