]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/binaries/transcript/types.ml
Fixed a call to auto, and commented the remaining part.
[helm.git] / helm / software / components / binaries / transcript / types.ml
index e51122b3f20e3aaa0788c4af47a123f373f72b0e..73420ee5921d987592cba96ebc646356b50b15f5 100644 (file)
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+type local = bool
+
 type inline_kind = Con | Ind | Var
 
 type item = Heading of (string * int)
@@ -31,8 +33,8 @@ type item = Heading of (string * int)
           | Unexport of string
           | BaseUri of string
          | Include of string
-          | Coercion of string
-         | Notation of string
+          | Coercion of (local * string)
+         | Notation of (local * string)
          | Inline of (inline_kind * string)
           | Verbatim of string
          | Discard of string