diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-10 17:09:29 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-10 17:09:29 +0000 |
| commit | c4a1f8efca6008e98837f15b5b4508486937543a (patch) | |
| tree | e6682b8e761f70d4d2fa10e5772e79e7a61744ea /parsing | |
| parent | 00588ac2c248155ee8cfd574ab517df235a5831a (diff) | |
- condition de garde (suite)
- commande Back
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2283 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -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) >> |