diff options
| author | herbelin | 2006-07-03 16:40:20 +0000 |
|---|---|---|
| committer | herbelin | 2006-07-03 16:40:20 +0000 |
| commit | 1e69c6a499757b05180205e84ed2bf6f1cbf7b2f (patch) | |
| tree | 0b6c57991e1bd849593f846ae8b91ce18d9f9194 /parsing | |
| parent | b7c3f0f2f57bcd0cc768c869d707b70f78c5bbfd (diff) | |
Extension des motifs disjonctifs au cas de disjonction de motifs multiples
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8997 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 3 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 4 |
2 files changed, 4 insertions, 3 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 2a975a9648..443a105113 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -274,7 +274,8 @@ GEXTEND Gram [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ] ; eqn: - [ [ pl = LIST1 pattern SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ] + [ [ pll = LIST0 LIST1 pattern LEVEL "99" SEP "," SEP "|"; + "=>"; rhs = lconstr -> (loc,pll,rhs) ] ] ; pattern: [ "200" RIGHTA [ ] diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 613fbfe780..92b07e08b1 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -186,12 +186,12 @@ let rec pr_patt sep inh p = let pr_patt = pr_patt mt - let pr_eqn pr (loc,pl,rhs) = spc() ++ hov 4 (pr_with_comments loc (str "| " ++ - hov 0 (prlist_with_sep sep_v (pr_patt ltop) pl ++ str " =>") ++ + hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl + ++ str " =>") ++ pr_sep_com spc (pr ltop) rhs)) let begin_of_binder = function |