- Procedural: we specify more unifiers for apply to help higher-order unification

[helm.git] / helm / software / components / binaries / transcript / grafiteParser.mly

diff --git a/helm/software/components/binaries/transcript/grafiteParser.mly b/helm/software/components/binaries/transcript/grafiteParser.mly
index 03ca0cdf47621ca0039e9691218628b41534f6bf..82295c69b553bc68f268a387f2127f49defb46ad 100644 (file)
--- 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 " ^ "") } */
-   ;
+  ;