diff options
| author | herbelin | 2004-04-08 15:21:25 +0000 |
|---|---|---|
| committer | herbelin | 2004-04-08 15:21:25 +0000 |
| commit | b0d199d2f08d42babd9061aff45a9bda0ac68b75 (patch) | |
| tree | 021987625a0f895fe5a2af4612828b69e1b2eae5 /translate | |
| parent | 866ef538adffca2bd4e3f8c6846907ebd377216a (diff) | |
Chgt role 2eme argument AList et implantation affichage motifs recursifs de notations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5663 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppconstrnew.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 164889adf8..8fdc68f93b 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -40,6 +40,7 @@ let lletin = 200 let lfix = 200 let larrow = 90 let lcast = 100 +let larg = 9 let lapp = 10 let lposint = 0 let lnegint = 35 (* must be consistent with Notation "- x" *) @@ -503,6 +504,10 @@ let rec pr sep inherited a = p ++ prlist (pr spc (lapp,L)) l2, lapp else p, lproj + | CAppExpl (_,(None,Ident (_,var)),[t]) + | CApp (_,(_,CRef(Ident(_,var))),[t,None]) + when var = Topconstr.ldots_var -> + hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg | CAppExpl (_,(None,f),l) -> pr_appexpl (pr mt) f l, lapp | CApp (_,(Some i,f),l) -> let l1,l2 = list_chop i l in |