G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body))
| IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
- | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = term ->
- G.NInverter (loc,name,indty)
+ | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
+ paramspec = OPT inverter_param_list ;
+ outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] ->
+ G.NInverter (loc,name,indty,paramspec,outsort)
| NLETCOREC ; defs = let_defs ->
nmk_rec_corec `CoInductive defs loc
| NLETREC ; defs = let_defs ->