| "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
%}
{ 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 " ^ "") } */
- ;
+ ;