+ | IDENT "nassert";
+ seqs = LIST0 [
+ hyps = LIST0
+ [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
+ | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
+ SYMBOL <:unicode<def>> ; bo = tactic_term ->
+ id,`Def (bo,ty)];
+ SYMBOL <:unicode<vdash>>;
+ concl = tactic_term -> (hyps,concl) ] ->
+ GrafiteAst.NAssert (loc, seqs)