- transcript: bugfix

[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 3163a6a07d5daf4bd9a4350b48fbdeb5eb667322..1e6855f554154fe068bdc99320286a5a8f26f6d6 100644 (file)
--- 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,7 +127,7 @@
          { 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)] }