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 /parsing/ppconstr.ml | |
| 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 'parsing/ppconstr.ml')
| -rw-r--r-- | parsing/ppconstr.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 7c573e07cc..ded6e823f9 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -219,6 +219,10 @@ let rec pr_cases_pattern _inh = function prlist_with_sep spc (pr_cases_pattern _inh) pl ++ str ")") | CPatAtom (_,Some c) -> pr_reference c | CPatAtom (_,None) -> str "_" + | CPatOr (_,pl) -> + str "(" ++ + hov 0 (prlist_with_sep pr_bar (pr_cases_pattern _inh) pl) ++ + str ")" | CPatNotation (_,"( _ )",[p]) -> str"("++ pr_cases_pattern _inh p ++ str")" | CPatNotation (_,s,env) -> fst (pr_patnotation pr_cases_pattern s env) |