- G.NAssert (loc, seqs)
- | IDENT "nauto"; params = auto_params -> G.NAuto (loc, params)
- | SYMBOL "/"; num = OPT NUMBER ; SYMBOL "/" ->
- let depth = match num with Some n -> n | None -> "1" in
- G.NAuto (loc, ([],["slir","";"depth",depth]))
+ 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))