Add syntax for non maximally inserted implicit arguments

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