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 /translate | |
| 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 'translate')
| -rw-r--r-- | translate/pptacticnew.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 327ec7d08..5fce8607d 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) -> |