diff options
| author | herbelin | 2003-12-04 17:24:01 +0000 |
|---|---|---|
| committer | herbelin | 2003-12-04 17:24:01 +0000 |
| commit | 8eb1626a3b5fdd9d0e455c8507210b6a83ea9213 (patch) | |
| tree | 6542068682ab41b0cd0863bfb792735dc3649952 | |
| 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
| -rw-r--r-- | parsing/g_ltacnew.ml4 | 12 | ||||
| -rw-r--r-- | translate/pptacticnew.ml | 6 |
2 files changed, 9 insertions, 9 deletions
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index 1f02415261..a39cfc4b55 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 "|"; "]" -> diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 327ec7d08b..5fce8607de 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -635,7 +635,7 @@ let ltactical = 3 in let lorelse = 2 in let llet = 1 in let lfun = 1 in -let labstract = 1 in +let labstract = 3 in let lmatch = 1 in let latom = 0 in let lcall = 1 in @@ -645,10 +645,10 @@ let ltatom = 1 in let rec pr_tac env inherited tac = let (strm,prec) = match tac with | TacAbstract (t,None) -> - str "abstract " ++ pr_tac env (labstract,E) t, labstract + str "abstract " ++ pr_tac env (labstract,L) t, labstract | TacAbstract (t,Some s) -> hov 0 - (str "abstract " ++ pr_tac env ltop t ++ spc () ++ + (str "abstract " ++ pr_tac env (labstract,L) t ++ spc () ++ str "using " ++ pr_id s), labstract | TacLetRecIn (l,t) -> |