- G.NTactic(loc,[G.NAssert (loc, seqs)])
- | IDENT "nauto"; params = auto_params ->
- G.NTactic(loc,[G.NAuto (loc, params)])
- | SYMBOL "/"; num = OPT NUMBER ;
- params = nauto_params; SYMBOL "/" ;
- just = OPT [ IDENT "by"; by =
- [ univ = tactic_term_list1 -> `Univ univ
- | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv
- | SYMBOL "_" -> `Trace ] -> by ] ->
- let depth = match num with Some n -> n | None -> "1" in
- (match just with
- | None ->
- G.NTactic(loc,
- [G.NAuto(loc,(None,["slir","";"depth",depth]@params))])
- | Some (`Univ univ) ->
- G.NTactic(loc,
- [G.NAuto(loc,(Some univ,["slir","";"depth",depth]@params))])
- | Some `EmptyUniv ->
- G.NTactic(loc,
- [G.NAuto(loc,(Some [],["slir","";"depth",depth]@params))])
- | Some `Trace ->
- G.NMacro(loc,
- G.NAutoInteractive (loc, (None,["slir","";"depth",depth]@params))))
- | IDENT "nintros" -> G.NMacro (loc, G.NIntroGuess loc)
- | IDENT "ncheck"; t = term -> G.NMacro(loc,G.NCheck (loc,t))
- | IDENT "screenshot"; fname = QSTRING ->
- G.NMacro(loc,G.Screenshot (loc, fname))