X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Ftypes.ml;h=7b17db7b202342c5fa218906d48e7ef7f6252640;hb=3bfc56cd9b5afe52c3abfbef886ce82efa3bb3a3;hp=73420ee5921d987592cba96ebc646356b50b15f5;hpb=876f16ec4e9080bad4e39bd9c203d6529dcf4f56;p=helm.git diff --git a/helm/software/components/binaries/transcript/types.ml b/helm/software/components/binaries/transcript/types.ml index 73420ee59..7b17db7b2 100644 --- a/helm/software/components/binaries/transcript/types.ml +++ b/helm/software/components/binaries/transcript/types.ml @@ -27,15 +27,25 @@ type local = bool type inline_kind = Con | Ind | Var +type input_kind = Gallina8 | Grafite + +type output_kind = Declarative | Procedural + +type source = string + +type prefix = string + +type flavour = Cic.object_flavour option + type item = Heading of (string * int) | Line of string | Comment of string | Unexport of string - | BaseUri of string | Include of string | Coercion of (local * string) | Notation of (local * string) - | Inline of (inline_kind * string) + | Section of (local * string * string) + | Inline of (local * inline_kind * source * prefix * flavour) | Verbatim of string | Discard of string