diff options
| author | herbelin | 2010-07-22 21:06:06 +0000 |
|---|---|---|
| committer | herbelin | 2010-07-22 21:06:06 +0000 |
| commit | 9b4927d7fdbbafa7ed372e152e7106b3055dfb99 (patch) | |
| tree | c395758164096f2a33ae8d57d2a2895cfa3203b8 /parsing | |
| parent | 53b06c3069c1234368d14de64ddd9382ff705f3b (diff) | |
Constrintern: unified push_name_env and push_loc_name_env; made
location dumping for binders uniformly treated in constrintern.ml (and
renamed the optional arg of interp_context from fail_anonymous to
global_level since the flag now also decides whether to dump binders as
global or local ones); added locations for the variables occurring in
the "as in" clauses;
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13314 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 8 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 6 |
2 files changed, 7 insertions, 7 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 087ae31ae6..e3c898284e 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -124,7 +124,7 @@ let ident_with = | _ -> err ()) | _ -> err ()) -let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None +let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None GEXTEND Gram GLOBAL: binder_constr lconstr constr operconstr sort global @@ -251,7 +251,7 @@ GEXTEND Gram po = return_type; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> - CLetTuple (loc,List.map snd lb,po,c1,c2) + CLetTuple (loc,lb,po,c1,c2) | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> CCases (loc, LetPatternStyle, None, [(c1,(None,None))], [(loc, [(loc,[p])], c2)]) @@ -308,14 +308,14 @@ GEXTEND Gram [ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ] ; pred_pattern: - [ [ ona = OPT ["as"; id=name -> snd id]; + [ [ ona = OPT ["as"; id=name -> id]; ty = OPT ["in"; t=lconstr -> t] -> (ona,ty) ] ] ; case_type: [ [ "return"; ty = operconstr LEVEL "100" -> ty ] ] ; return_type: - [ [ a = OPT [ na = OPT["as"; id=name -> snd id]; + [ [ a = OPT [ na = OPT["as"; na=name -> na]; ty = case_type -> (na,ty) ] -> match a with | None -> None, None diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 2d63b20bb5..6a4d9757d8 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -365,7 +365,7 @@ let tm_clash = function let pr_asin pr (na,indnalopt) = (match na with (* Decision of printing "_" or not moved to constrextern.ml *) - | Some na -> spc () ++ str "as " ++ pr_name na + | Some na -> spc () ++ str "as " ++ pr_lname na | None -> mt ()) ++ (match indnalopt with | None -> mt () @@ -384,7 +384,7 @@ let pr_return_type pr po = pr_case_type pr po let pr_simple_return_type pr na po = (match na with - | Some (Name id) -> + | Some (_,Name id) -> spc () ++ str "as " ++ pr_id id | _ -> mt ()) ++ pr_case_type pr po @@ -518,7 +518,7 @@ let pr pr sep inherited a = hv 0 ( str "let " ++ hov 0 (str "(" ++ - prlist_with_sep sep_v pr_name nal ++ + prlist_with_sep sep_v pr_lname nal ++ str ")" ++ pr_simple_return_type (pr mt) na po ++ str " :=" ++ pr spc ltop c ++ str " in") ++ |