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/ppconstr.ml | |
| 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/ppconstr.ml')
| -rw-r--r-- | parsing/ppconstr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) |