diff options
| author | pboutill | 2012-02-29 13:33:13 +0000 |
|---|---|---|
| committer | pboutill | 2012-02-29 13:33:13 +0000 |
| commit | 4ad3f3170796957e3701c62df5678fae385ca2fd (patch) | |
| tree | 9f5cfeebfc88d481b7c65f77429ba711f2562540 /parsing | |
| parent | 32c7a28aa909ed04993f4701702db5e6272bc7ab (diff) | |
In the syntax of pattern matching, "in" clauses are patterns.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15000 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 4 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index ad9cba880b..af63e215fa 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -243,7 +243,7 @@ GEXTEND Gram | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> CCases (loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, None))], [(loc, [(loc, [p])], c2)]) - | "let"; "'"; p=pattern; "in"; t = operconstr LEVEL "200"; + | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> CCases (loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, Some t))], [(loc, [(loc, [p])], c2)]) @@ -294,7 +294,7 @@ GEXTEND Gram ; pred_pattern: [ [ ona = OPT ["as"; id=name -> id]; - ty = OPT ["in"; t=lconstr -> t] -> (ona,ty) ] ] + ty = OPT ["in"; t=pattern -> t] -> (ona,ty) ] ] ; case_type: [ [ "return"; ty = operconstr LEVEL "100" -> ty ] ] diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 16820efdcb..1f37e36dfc 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -371,7 +371,7 @@ let pr_asin pr (na,indnalopt) = | None -> mt ()) ++ (match indnalopt with | None -> mt () - | Some t -> spc () ++ str "in " ++ pr lsimple t) + | Some t -> spc () ++ str "in " ++ pr_patt lsimple t) let pr_case_item pr (tm,asin) = hov 0 (pr (lcast,E) tm ++ pr_asin pr asin) |