- Improve [Context] vernacular to allow arbitrary binders, not just

classes, and simplify the implementation.
- Experimental syntax {{ cl : Class args }} and (( cl : Class args ))
which respectively make cl an implicit or explicit argument ({{ }} is
equivalent to [ ]). Could be extended to any type of binder, eg. 
[Definition flip ((R : relation carrier)) : relation carrier := ...].
The idea behind double brackets is to distinguish macro-binders which 
perform implicit generalization from regular binders. It could also save
[ ] for other uses.
- Fix bug #1901 about {} binders in records.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11210 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 12 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 3f437721a..476c0913f 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -398,7 +398,12 @@ GEXTEND Gram
         [LocalRawAssum ([id],Default Implicit,c)]
     | "{"; id=name; idl=LIST1 name; "}" -> 
         List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
-    | "["; tc = LIST1 typeclass_constraint_binder SEP ","; "]" -> tc
+    | "("; "("; tc = LIST1 typeclass_constraint SEP "," ; ")"; ")" ->
+	List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Explicit, b), t)) tc
+    | "{"; "{"; tc = LIST1 typeclass_constraint SEP "," ; "}"; "}" ->
+	List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Implicit, b), t)) tc
+    | "["; tc = LIST1 typeclass_constraint SEP ","; "]" -> 
+	List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Implicit, b), t)) tc
     ] ]
   ;
   binder:
@@ -407,21 +412,14 @@ GEXTEND Gram
       | "{"; idl=LIST1 name; ":"; c=lconstr; "}" -> (idl,Default Implicit,c) 
     ] ]
   ;
-  typeclass_constraint_binder:
-    [ [ tc = typeclass_constraint ->
-      let (n,(b,b'),t) = tc in
-	LocalRawAssum ([n], TypeClass (b,b'), t)
-    ] ]
-  ;
-
   typeclass_constraint:
-    [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), (Implicit, Explicit), c
+    [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), Explicit, c
       | "{"; id = name; "}"; ":" ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
-	  id, (Implicit, expl), c
+	  id, expl, c
       | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
-	  (loc, Name iid), (Explicit, expl), c
+	  (loc, Name iid), expl, c
       | c = operconstr LEVEL "200" ->
-	  (loc, Anonymous), (Implicit, Implicit), c
+	  (loc, Anonymous), Implicit, c
     ] ]
   ;