X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2FgrafiteParser.mly;h=82295c69b553bc68f268a387f2127f49defb46ad;hb=b519aa529779c0a4625eb43fa9557862d8cc6617;hp=3163a6a07d5daf4bd9a4350b48fbdeb5eb667322;hpb=3bfc56cd9b5afe52c3abfbef886ce82efa3bb3a3;p=helm.git

diff --git a/helm/software/components/binaries/transcript/grafiteParser.mly b/helm/software/components/binaries/transcript/grafiteParser.mly
index 3163a6a07..82295c69b 100644
--- a/helm/software/components/binaries/transcript/grafiteParser.mly
+++ b/helm/software/components/binaries/transcript/grafiteParser.mly
@@ -42,7 +42,7 @@
         | "lemma"       -> T.Con, Some `Lemma
         | "fact"        -> T.Con, Some `Fact 
         | "remark"      -> T.Con, Some `Remark        
-        | "variant"     -> T.Con, None
+        | "variant"     -> T.Con, Some `Variant
 	| _             -> assert false
 
 %}
@@ -127,15 +127,14 @@
          { out "OK" $1; [T.Verbatim $1] }
       | TH SPC id line drops
          { out "TH" $3;
-	   let a, b = mk_flavour $1 in [T.Inline (true, 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
-         { [] }
+      | 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 " ^ "") } */
-   ;
+  ;