NTactics.elim_tac
~what:(text,prefix_len,what)
~where:(text,prefix_len,where)
- | GrafiteAst.NId _ -> fun x -> x
+ | GrafiteAst.NId _ -> (fun x -> x)
+ | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
;;
let rec eval_command = {ec_go = fun ~disambiguate_command opts status