From 6cd832e28c48382cc9321825cc83db36f96ff8d5 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 15 Jan 2008 01:02:48 +0000
Subject: Generalize instance declarations to any context, better name
 handling. Add hole kind info for topconstrs. Derive eta_expansion from
 functional extensionality axiom.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10439 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/typeclasses.mli | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'pretyping/typeclasses.mli')

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 47cb93a149..ec3350a586 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -26,8 +26,9 @@ type typeclass = {
   (* Name of the class. FIXME: should not necessarily be globally unique. *)
   cl_name : identifier;
 
-  (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : (identifier option * named_declaration) list; 
+  (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The boolean indicates if the 
+     typeclass argument is a direct superclass. *)
+  cl_context : ((identifier * bool) option * named_declaration) list; 
 
   cl_params : int; (* This is the length of the suffix of the context which should be considered explicit parameters. *)
 
-- 
cgit v1.2.3