diff options
| author | herbelin | 2004-09-09 13:27:03 +0000 |
|---|---|---|
| committer | herbelin | 2004-09-09 13:27:03 +0000 |
| commit | ce7e64328553ac71f2630816cfb8baa930ea471e (patch) | |
| tree | e0669306e771ebc7e5b9a7712212c39047e44d2e /translate | |
| parent | 1795451a803ffa38d9b5cbf38d93cc7df687c11f (diff) | |
Ajout de or-pattern pour le match-with v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6088 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppconstrnew.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 47a92f7cae..35cd2ea2c6 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -160,6 +160,7 @@ let pr_or_var pr = function | Genarg.ArgVar (loc,s) -> pr_lident (loc,s) let las = lapp +let lpator = 100 let rec pr_patt sep inh p = let (strm,prec) = match p with @@ -170,6 +171,8 @@ let rec pr_patt sep inh p = pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp | CPatAtom (_,None) -> str "_", latom | CPatAtom (_,Some r) -> pr_reference r, latom + | CPatOr (_,pl) -> + hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator | CPatNotation (_,"( _ )",[p]) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom | CPatNotation (_,s,env) -> pr_patnotation (pr_patt mt) s env |