G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular))
| IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular))
| IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))