From a1d00fa77939f99dd5e7ddd41c8ecf64e8af4fa1 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Mon, 2 Dec 2019 12:52:39 +0100
Subject: Add syntax for non maximally inserted implicit arguments

---
 printing/ppconstr.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'printing/ppconstr.ml')

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
-- 
cgit v1.2.3