- | 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 [])