diff options
| author | msozeau | 2008-01-17 16:04:42 +0000 |
|---|---|---|
| committer | msozeau | 2008-01-17 16:04:42 +0000 |
| commit | cd21f033922b22f855111e171ece9591009cf15b (patch) | |
| tree | 5bd3a2f04a8fda4db42df0fc8aa9e5cb387cd48b /parsing | |
| 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')
| -rw-r--r-- | parsing/g_constr.ml4 | 12 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 6 |
2 files changed, 14 insertions, 4 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index e55024b516..9972d9e248 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -201,11 +201,15 @@ GEXTEND Gram ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> CLetTuple (loc,List.map snd lb,po,c1,c2) - | "dest"; c1 = operconstr LEVEL "200"; "as"; p=pattern; + | "let"; "|"; p=pattern; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> - let loc' = cases_pattern_expr_loc p in - CCases (loc, None, [(c1, (None, None))], - [loc, [loc',[p]], c2]) + CLetPattern (loc, p, 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, [loc',[p]], c2]) | "if"; c=operconstr LEVEL "200"; po = return_type; "then"; b1=operconstr LEVEL "200"; "else"; b2=operconstr LEVEL "200" -> diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 8dff6dbf53..7d0d085938 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) *) |