Fixes in handling of implicit arguments:

- Now [ id : Class foo ] makes id an explicit argument, 
  and [ Class foo ] is equivalent to [ {someid} : Class foo ].
  This makes declarations such as "Class Ord [ eq : Eq a ]" have
  sensible implicit args.
- Better handling of {} in class and record declarations, refactorize 
  code for declaring structures and classes.  
- Fix merging of implicit arguments information on section closing.


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

4 files changed, 13 insertions, 11 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 6b6b4871c..3f437721a 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -409,17 +409,19 @@ GEXTEND Gram
   ;
   typeclass_constraint_binder:
     [ [ tc = typeclass_constraint ->
-      let (n,bk,t) = tc in
-	LocalRawAssum ([n], TypeClass bk, t)
+      let (n,(b,b'),t) = tc in
+	LocalRawAssum ([n], TypeClass (b,b'), t)
     ] ]
   ;
 
   typeclass_constraint:
-    [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), Explicit, c
-    | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
-	(loc, Name iid), expl, c
-    | c = operconstr LEVEL "200" ->
-	(loc, Anonymous), Implicit, c
+    [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), (Implicit, Explicit), c
+      | "{"; id = name; "}"; ":" ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
+	  id, (Implicit, expl), c
+      | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
+	  (loc, Name iid), (Explicit, expl), c
+      | c = operconstr LEVEL "200" ->
+	  (loc, Anonymous), (Implicit, Implicit), c
     ] ]
   ;
   
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index aaf4324e2..19cb28778 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 * constr_expr) Gram.Entry.e
+    val typeclass_constraint : (name located * (binding_kind * binding_kind) * constr_expr) Gram.Entry.e
     val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
   end
 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 04b700236..912406f3f 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -219,13 +219,13 @@ let surround_binder k p =
   match k with
       Default Explicit -> hov 1 (str"(" ++ p ++ str")")
     | Default Implicit -> hov 1 (str"{" ++ p ++ str"}")
-    | TypeClass b -> hov 1 (str"[" ++ p ++ str"]")
+    | TypeClass _ -> hov 1 (str"[" ++ p ++ str"]")
 
 let surround_implicit k p =
   match k with
       Default Explicit -> p
     | Default Implicit -> (str"{" ++ p ++ str"}")
-    | TypeClass b -> (str"[" ++ p ++ str"]")
+    | TypeClass _ -> (str"[" ++ p ++ str"]")
 
 let pr_binder many pr (nal,k,t) =
   match t with
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index e27a93b33..6bd795ed5 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -139,7 +139,7 @@ let mlexpr_of_binding_kind = function
 
 let mlexpr_of_binder_kind = function
   | Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >>
-  | Topconstr.TypeClass b -> <:expr< Topconstr.TypeClass $mlexpr_of_binding_kind b$ >>
+  | Topconstr.TypeClass (b,b') -> <:expr< Topconstr.TypeClass $mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_binding_kind (b,b')$ >>
 
 let rec mlexpr_of_constr = function
   | Topconstr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) ->