+ | GrafiteAst.NNonPunctuationTactical (_, non_punct, punct) ->
+ (match status.GrafiteTypes.ng_status with
+ | GrafiteTypes.CommandMode _ -> assert false
+ | GrafiteTypes.ProofMode nstatus ->
+ let nstatus = eval_ng_non_punct (text,prefix_len,non_punct) nstatus in
+ let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in
+ NTacStatus.pp_tac_status nstatus;
+ { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus },
+ `New [])