diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 66c8e0170..accb5d958 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -453,7 +453,9 @@ GEXTEND Gram | IDENT "Reset"; IDENT "Initial" -> <:ast< (ResetInitial) >> | IDENT "Reset"; IDENT "Section"; id = identarg -> <:ast< (ResetSection $id) >> - + | IDENT "Back" -> <:ast<(Back)>> + | IDENT "Back"; n = numarg -> <:ast<(Back $n)>> + (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> <:ast< (DebugOn) >> | IDENT "Debug"; IDENT "Off" -> <:ast< (DebugOff) >> |