diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-04 17:24:01 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-04 17:24:01 +0000 |
| commit | 8eb1626a3b5fdd9d0e455c8507210b6a83ea9213 (patch) | |
| tree | 6542068682ab41b0cd0863bfb792735dc3649952 /parsing/g_ltacnew.ml4 | |
| parent | aa357d601d440a2e22de61299e0f87e79bed27fd (diff) | |
Symetrisation parsing/printing 'abstract'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5066 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_ltacnew.ml4')
| -rw-r--r-- | parsing/g_ltacnew.ml4 | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index 1f0241526..a39cfc4b5 100644 --- a/parsing/g_ltacnew.ml4 +++ b/parsing/g_ltacnew.ml4 @@ -84,7 +84,12 @@ GEXTEND Gram | IDENT "do"; n = natural; ta = tactic_expr -> TacDo (n,ta) | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta | IDENT "progress"; ta = tactic_expr -> TacProgress ta - | IDENT "info"; tc = tactic_expr -> TacInfo tc ] + | IDENT "info"; tc = tactic_expr -> TacInfo tc +(*To do: put Abstract in Refiner*) + | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None) + | IDENT "abstract"; tc = NEXT; "using"; s = base_ident -> + TacAbstract (tc,Some s) ] +(*End of To do*) | "2" RIGHTA [ ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ] | "1" RIGHTA @@ -101,11 +106,6 @@ GEXTEND Gram TacMatchContext (true,mrl) | "match"; c = tactic_expr; "with"; mrl = match_list; "end" -> TacMatch (c,mrl) -(*To do: put Abstract in Refiner*) - | IDENT "abstract"; tc = tactic_expr -> TacAbstract (tc,None) - | IDENT "abstract"; tc = tactic_expr; "using"; s = base_ident -> - TacAbstract (tc,Some s) -(*End of To do*) | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> TacFirst l | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> |