]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/binaries/transcript/grafiteParser.mly
Propagation of changes to grafiteAst.
[helm.git] / matita / components / binaries / transcript / grafiteParser.mly
index 82295c69b553bc68f268a387f2127f49defb46ad..2f4d1e264c09a3cbcc2cf4e8103a64b4b1ff0109 100644 (file)
          { out "OK" $1; [T.Verbatim $1] }
       | TH SPC id line drops
          { out "TH" $3;
-          let a, b = mk_flavour $1 in [T.Inline (false, a, $3, "", b, [])] 
+          let a, b = mk_flavour $1 in [T.Inline (false, a, $3, "", b)] 
         }
       | UNX line drops { out "UNX" $1; [T.Verbatim ($1 ^ $2 ^ $3)] }
       | PS steps       { out "PS" $2; [] }