grafite_ncommand: [ [
IDENT "qed" ; b = OPT SYMBOL "-" ->
let b = match b with None -> true | Some _ -> false in
- if not b then G.NQed (loc,b)
+ G.NQed (loc,b)
| nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))