diff options
| author | herbelin | 2008-01-05 19:07:05 +0000 |
|---|---|---|
| committer | herbelin | 2008-01-05 19:07:05 +0000 |
| commit | bd9dc4089bdf76437a358d8c1a282f67558905be (patch) | |
| tree | 56116bcf7d47b7b356a11daaf93af59e8f770cc9 /parsing | |
| parent | d5d41c634dc1e3e7f07b3a465bc80b4eb5ea856f (diff) | |
Correction bug #1749 (datant de l'implantation des or-patterns) +
amélioration message d'erreur si nombre de pattern incorrect.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10427 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 8 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 1 |
2 files changed, 7 insertions, 2 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index c649b58466..a7d905032b 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -203,8 +203,9 @@ GEXTEND Gram CLetTuple (loc,List.map snd lb,po,c1,c2) | "dest"; c1 = operconstr LEVEL "200"; "as"; p=pattern; "in"; c2 = operconstr LEVEL "200" -> + let loc' = cases_pattern_expr_loc p in CCases (loc, None, [(c1, (None, None))], - [loc, [[p]], c2]) + [loc, [loc',[p]], c2]) | "if"; c=operconstr LEVEL "200"; po = return_type; "then"; b1=operconstr LEVEL "200"; "else"; b2=operconstr LEVEL "200" -> @@ -274,8 +275,11 @@ GEXTEND Gram branches: [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ] ; + mult_pattern: + [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> (loc,pl) ] ] + ; eqn: - [ [ pll = LIST1 LIST1 pattern LEVEL "99" SEP "," SEP "|"; + [ [ pll = LIST1 mult_pattern SEP "|"; "=>"; rhs = lconstr -> (loc,pll,rhs) ] ] ; pattern: diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 85bf11806e..ed4386ada0 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -197,6 +197,7 @@ let rec pr_patt sep inh p = let pr_patt = pr_patt mt let pr_eqn pr (loc,pl,rhs) = + let pl = List.map snd pl in spc() ++ hov 4 (pr_with_comments loc (str "| " ++ |