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