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 --- pretyping/typeclasses.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'pretyping/typeclasses.mli') diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index f77be52932..60b5da8226 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -32,8 +32,6 @@ type typeclass = { The boolean indicates if the typeclass argument is a direct superclass. *) cl_context : ((global_reference * bool) option * rel_declaration) list; - cl_params : int; (* This is the length of the suffix of the context which should be considered explicit parameters. *) - (* Context of definitions and properties on defs, will not be shared *) cl_props : rel_context; -- cgit v1.2.3