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

1 files changed, 2 insertions, 2 deletions

diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 04b700236a..912406f3f1 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