diff options
| author | herbelin | 2003-09-10 16:57:33 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-10 16:57:33 +0000 |
| commit | 821c13ab8599fc6fea4c058d12d88b2aaa3d682c (patch) | |
| tree | 27d8926983c84ad0d69498478ee5a9801149738c /translate | |
| parent | bd35666d45c7f9e811509d2e256e2ddce758a5ee (diff) | |
Passage des projections au niveau 1
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4349 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppconstrnew.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 438c1cc050..e6385e3d33 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -41,9 +41,9 @@ let larrow = 80 let lnegint = 40 let lcast = 100 let lapp = 10 -let lproj = 9 let ltop = (200,E) -let lsimple = (9,E) +let lproj = 1 +let lsimple = (1,E) let prec_less child (parent,assoc) = if parent < 0 && child = lprod then true @@ -374,7 +374,7 @@ let pr_simple_return_type pr na po = pr_case_type pr po let pr_proj pr pr_app a f l = - hov 0 (pr (lproj,E) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")") + hov 0 (pr lsimple a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")") let pr_appexpl pr f l = hov 2 ( |