X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2FgrafiteParser.mly;h=82295c69b553bc68f268a387f2127f49defb46ad;hb=0ef9250d71eacd6b1022194128e6acfb74d52aac;hp=03ca0cdf47621ca0039e9691218628b41534f6bf;hpb=d3548c16f481b14ce94e64c790bc767c59590050;p=helm.git diff --git a/helm/software/components/binaries/transcript/grafiteParser.mly b/helm/software/components/binaries/transcript/grafiteParser.mly index 03ca0cdf4..82295c69b 100644 --- a/helm/software/components/binaries/transcript/grafiteParser.mly +++ b/helm/software/components/binaries/transcript/grafiteParser.mly @@ -129,13 +129,12 @@ { out "TH" $3; 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 - { [] } + | UNX line drops { out "UNX" $1; [T.Verbatim ($1 ^ $2 ^ $3)] } + | PS steps { out "PS" $2; [] } + | QED FS { [] } ; items: | EOF { [] } | item items { $1 @ $2 } /* | error { out "ERROR" ""; failwith ("item id " ^ "") } */ - ; + ;