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

---
 parsing/g_constr.mlg | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index af1e973261..dcc3a87b11 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -205,7 +205,7 @@ GRAMMAR EXTEND Gram
       | "{"; c = binder_constr ; "}" ->
         { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) }
       | "`{"; c = operconstr LEVEL "200"; "}" ->
-        { CAst.make ~loc @@ CGeneralization (Implicit, None, c) }
+        { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) }
       | "`("; c = operconstr LEVEL "200"; ")" ->
         { CAst.make ~loc @@ CGeneralization (Explicit, None, c) } ] ]
   ;
@@ -431,17 +431,27 @@ GRAMMAR EXTEND Gram
       | "("; id = name; ":"; t = lconstr; ":="; c = lconstr; ")" ->
         { [CLocalDef (id,c,Some t)] }
       | "{"; id = name; "}" ->
-        { [CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] }
+        { [CLocalAssum ([id],Default MaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] }
       | "{"; id = name; idl = LIST1 name; ":"; c = lconstr; "}" ->
-        { [CLocalAssum (id::idl,Default Implicit,c)] }
+        { [CLocalAssum (id::idl,Default MaxImplicit,c)] }
       | "{"; id = name; ":"; c = lconstr; "}" ->
-        { [CLocalAssum ([id],Default Implicit,c)] }
+        { [CLocalAssum ([id],Default MaxImplicit,c)] }
       | "{"; id = name; idl = LIST1 name; "}" ->
-        { List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) }
+        { List.map (fun id -> CLocalAssum ([id],Default MaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) }
+      | "["; id = name; "]" ->
+        { [CLocalAssum ([id],Default NonMaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] }
+      | "["; id = name; idl = LIST1 name; ":"; c = lconstr; "]" ->
+        { [CLocalAssum (id::idl,Default NonMaxImplicit,c)] }
+      | "["; id = name; ":"; c = lconstr; "]" ->
+        { [CLocalAssum ([id],Default NonMaxImplicit,c)] }
+      | "["; id = name; idl = LIST1 name; "]" ->
+        { List.map (fun id -> CLocalAssum ([id],Default NonMaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) }
       | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
         { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Explicit, b), t)) tc }
       | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
-        { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, b), t)) tc }
+        { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (MaxImplicit, b), t)) tc }
+      | "`["; tc = LIST1 typeclass_constraint SEP "," ; "]" ->
+        { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (NonMaxImplicit, b), t)) tc }
       | "'"; p = pattern LEVEL "0" ->
         { let (p, ty) =
             match p.CAst.v with
-- 
cgit v1.2.3