return_tactic loc (TacticAst.Transitivity t)
]
];
- tactical0: [ [ t = tactical; SYMBOL ";;" -> t ] ];
+ tactical0: [ [ t = tactical; SYMBOL ";;" -> return_tactical loc t ] ];
tactical:
[ "command" NONA
[ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
return_command loc (TacticAst.Undo (int_opt steps))
| [ IDENT "redo" | IDENT "Redo" ]; steps = OPT NUM ->
return_command loc (TacticAst.Redo (int_opt steps))
+ | [ IDENT "baseuri" | IDENT "Baseuri" ]; uri = OPT QSTRING ->
+ return_command loc (TacticAst.Baseuri uri)
| [ IDENT "check" | IDENT "Check" ]; t = term ->
return_command loc (TacticAst.Check t)
]