- 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

4 files changed, 13 insertions, 19 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 3f437721a8..476c0913f9 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
     ] ]
   ;
   
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c128d7ae1e..83b238953b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -491,7 +491,7 @@ GEXTEND Gram
 	 props = typeclass_field_types ->
 	   VernacClass (qid, pars, s, (match sup with None -> [] | Some l -> l), props)
 	     
-      | IDENT "Context"; c = typeclass_context -> 
+      | IDENT "Context"; c = binders_let -> 
 	  VernacContext c
 	    
       | global = [ IDENT "Global" -> true | -> false ];
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 19cb287781..aaf4324e2c 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -166,7 +166,7 @@ module Constr :
     val binder_let : local_binder list Gram.Entry.e
     val binders_let : local_binder list Gram.Entry.e
     val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
-    val typeclass_constraint : (name located * (binding_kind * binding_kind) * constr_expr) Gram.Entry.e
+    val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
     val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
   end
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 3ec225ddce..1060928d12 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -403,9 +403,6 @@ let pr_constrarg c = spc () ++ pr_constr c in
 let pr_lconstrarg c = spc () ++ pr_lconstr c in
 let pr_intarg n = spc () ++ int n in
 let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in
-let pr_lname_lident_constr (oi,bk,a) = 
-  (match snd oi with Anonymous -> mt () | Name id -> pr_lident (fst oi, id) ++ spc () ++ str":" ++ spc ()) 
-  ++ pr_lconstr a in
 let pr_instance_def sep (i,l,c) = pr_lident i ++ prlist_with_sep spc pr_lident l 
   ++ sep ++ pr_constrarg c in
 
@@ -717,8 +714,7 @@ let rec pr_vernac = function
  | VernacContext l ->
      hov 1 (
        str"Context" ++ spc () ++ str"[" ++ spc () ++
-	 prlist_with_sep (fun () -> str"," ++ spc()) pr_lname_lident_constr l ++
-	 spc () ++ str "]")
+	 pr_and_type_binders_arg l ++ spc () ++ str "]")
 	      
 
  | VernacDeclareInstance id ->