- G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular))
- | IDENT "axiom"; 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),
+ true)
+ | IDENT "axiom"; i = index; name = IDENT; SYMBOL ":"; typ = term ->
+ G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular),i)