From ff03e8dd0de507be82e58ed5e8fd902dfd7caf4b Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 4 Jul 2008 14:38:44 +0000 Subject: 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 --- parsing/ppconstr.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'parsing/ppconstr.ml') 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 -- cgit v1.2.3