Erroneously declared coercion removed

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

diff --git a/components/binaries/transcript/types.ml b/components/binaries/transcript/types.ml
index d7770ade78e417955a8022b6569b11835103626d..de7c1036e8cc26ab20e6316e7c157eb7ed95c3c4 100644 (file)
--- a/components/binaries/transcript/types.ml
+++ b/components/binaries/transcript/types.ml
@@ -23,16 +23,24 @@
  * http://cs.unibo.it/helm/.
  *)
 
+type local = bool
+
 type inline_kind = Con | Ind | Var
 
+type source = string
+
+type prefix = string
+
 type item = Heading of (string * int)
-          | Comment of string
+          | Line of string
+         | Comment of string
           | Unexport of string
           | BaseUri of string
          | Include of string
-          | Coercion of string
-         | Notation of string
-         | Inline of (inline_kind * string)
+          | Coercion of (local * string)
+         | Notation of (local * string)
+         | Section of (local * string * string)
+         | Inline of (local * inline_kind * source * prefix)
           | Verbatim of string
          | Discard of string