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

1 files changed, 9 insertions, 8 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index e253410dee..a1183c97bb 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -33,7 +33,7 @@ type typeclass = {
   cl_name : identifier;
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : (identifier option * named_declaration) list; 
+  cl_context : ((identifier * bool) option * named_declaration) list; 
 
   cl_params: int;
 
@@ -298,13 +298,14 @@ let resolve_typeclasses ?(check=true) env sigma evd =
   in sat evd
 
 let class_of_constr c = 
-  match kind_of_term c with
-      App (c, _) -> 
-	(match kind_of_term c with
-	    Ind ind -> (try Some (class_of_inductive ind) with Not_found -> None)
-	  | _ -> None)
-    | _ -> None
-
+  let extract_ind c =
+    match kind_of_term c with
+	Ind ind -> (try Some (class_of_inductive ind) with Not_found -> None)
+      | _ -> None
+  in
+    match kind_of_term c with
+	App (c, _) -> extract_ind c
+      | _ -> extract_ind c
 
 type substitution = (identifier * constr) list