diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-17 16:04:42 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-17 16:04:42 +0000 |
| commit | cd21f033922b22f855111e171ece9591009cf15b (patch) | |
| tree | 5bd3a2f04a8fda4db42df0fc8aa9e5cb387cd48b /parsing/ppconstr.ml | |
| parent | 6a018defe4db779522f6ab6ae31f04adb886d49c (diff) | |
Add new LetPattern construct to replace dest. syntax: let| pat := t in b is backwards compatible. Update CHANGES with things i've done.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10446 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ppconstr.ml')
| -rw-r--r-- | parsing/ppconstr.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 8dff6dbf5..7d0d08593 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -36,6 +36,7 @@ let lprod = 200 let llambda = 200 let lif = 200 let lletin = 200 +let lletpattern = 200 let lfix = 200 let larrow = 90 let lcast = 100 @@ -570,6 +571,11 @@ let rec pr sep inherited a = pr spc ltop c ++ str " in") ++ pr spc ltop b), lletin + | CLetPattern (_, p, c, b) -> + hv 0 ( + str "let| " ++ + hov 0 (pr_patt ltop p ++ str " :=" ++ pr spc ltop c ++ str " in") ++ + pr spc ltop b), lletpattern | CIf (_,c,(na,po),b1,b2) -> (* On force les parenthèses autour d'un "if" sous-terme (même si le parsing est lui plus tolérant) *) |