diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-19 10:58:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-19 11:57:21 +0200 |
| commit | a67bd7f93224c61b6a59459ea1114a6670daa857 (patch) | |
| tree | 59ec2885f0059baa24403d37eaf559b59e5f82bb /printing/ppconstr.ml | |
| parent | b663b735adaf546192ff5b25b608dda55e05f3d8 (diff) | |
Taking into account binding patterns when agglutinating sequences of binders.
Supporting accordingly printing of sequences of binders including binding
patterns.
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index be92372ac..7aa6d4858 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -349,8 +349,8 @@ end) = struct | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in surround (pr_lname na ++ pr_opt_type pr_c topt ++ str":=" ++ cut() ++ pr_c c) - | LocalPattern _ -> - assert false + | LocalPattern (loc,p,tyo) -> + str "'" ++ pr_patt lsimplepatt p let pr_undelimited_binders sep pr_c = prlist_with_sep sep (pr_binder_among_many pr_c) @@ -360,10 +360,8 @@ end) = struct match bl with | [LocalRawAssum (nal,k,t)] -> pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t) - | LocalRawAssum _ :: _ as bdl -> + | (LocalRawAssum _ | LocalPattern _) :: _ as bdl -> pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl - | LocalPattern (loc,p,tyo) :: _ -> - str "'" ++ pr_patt ltop p | _ -> assert false let pr_binders_gen pr_c sep is_open = |