]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/binaries/transcript/types.ml
cicDischarge: new module for discharging the explicit variables occurring in a
[helm.git] / helm / software / components / binaries / transcript / types.ml
index f0c8212bc47c3271c94045d895592f3a785aacbc..fbe112a83616ae7709c16727fb4757772bec1178 100644 (file)
@@ -33,16 +33,17 @@ 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)
          | Section of (local * string * string)
-         | Inline of (local * inline_kind * source * prefix)
+         | Inline of (local * inline_kind * source * prefix * flavour)
           | Verbatim of string
          | Discard of string