diff options
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index b55a41471a..2416819a6a 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -143,7 +143,8 @@ let tag_var = tag Tag.variable let pr_generalization bk ak c = let hd, tl = match bk with - | Implicit -> "{", "}" + | NonMaxImplicit -> "[", "]" + | MaxImplicit -> "{", "}" | Explicit -> "(", ")" in (* TODO: syntax Abstraction Kind *) str "`" ++ str hd ++ c ++ str tl @@ -324,12 +325,14 @@ let tag_var = tag Tag.variable let surround_impl k p = match k with | Explicit -> str"(" ++ p ++ str")" - | Implicit -> str"{" ++ p ++ str"}" + | NonMaxImplicit -> str"[" ++ p ++ str"]" + | MaxImplicit -> str"{" ++ p ++ str"}" let surround_implicit k p = match k with | Explicit -> p - | Implicit -> (str"{" ++ p ++ str"}") + | NonMaxImplicit -> str"[" ++ p ++ str"]" + | MaxImplicit -> (str"{" ++ p ++ str"}") let pr_binder many pr (nal,k,t) = match k with |