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

3 files changed, 14 insertions, 10 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3689ae174a..c9d44e3dc9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -670,6 +670,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let j = pretype empty_tycon env evdref ([],[]) c in
     let evd,_ = consider_remaining_unif_problems env !evdref in
     let j = j_nf_evar (evars_of evd) j in
+    let evd = Typeclasses.resolve_typeclasses env (evars_of evd) evd in
+    let j = j_nf_evar (evars_of evd) j in
     check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
     j
 
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
 
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. *)