Various fixes on typeclasses:

- Better interface in constrintern w.r.t. evars used during typechecking
- Add "unsatisfiable_constraints" exception which gives back the raw
evar_map that was not satisfied during typeclass search (presentation
could be improved).
- Correctly infer the minimal sort for typeclasses declared as
definitions (everything was in type before).
- Really handle priorities in typeclass eauto: goals produced with higher
priority (lowest number) instances are tried before other of lower
priority goals, regardless of the number of subgoals.
- Change inverse to a notation for flip, now that universe polymorphic
definitions are handled correctly. 
- Add EquivalenceDec class similar to SetoidDec, declaring decision
procedures for equivalences.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10724 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 8 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 0c99fe16ec..d652436802 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -136,12 +136,12 @@ let new_instance ctx (instid, bk, cl) props pri =
   let gen_ctx = Implicit_quantifiers.binder_list_of_ids gen_ids in
   let ctx, avoid = Classes.name_typeclass_binders bound ctx in
   let ctx = List.rev_append gen_ctx ctx in
-  let k, ctx', subst = 
+  let k, ctx', imps, subst = 
     let c = Command.generalize_constr_expr tclass ctx in
-    let c' = interp_type_evars isevars env c in
+    let c', imps = interp_type_evars_impls ~evdref:isevars env c in
     let ctx, c = Classes.decompose_named_assum c' in
     let cl, args = Typeclasses.dest_class_app c in
-      cl, ctx, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
+      cl, ctx, imps, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
   in
   let id = 
     match snd instid with
@@ -194,11 +194,13 @@ let new_instance ctx (instid, bk, cl) props pri =
       Evarutil.nf_isevar !isevars t
   in
   isevars := undefined_evars !isevars;
-  let imps = 
-    Util.list_map_i 
-      (fun i (na, b, t) -> ExplByPos (i, Some na), (true, true))
-      1 ctx'
-  in
+(*   let imps =  *)
+(*     Util.list_map_i  *)
+(*       (fun i binder -> *)
+(* 	match binder with *)
+(* 	ExplByPos (i, Some na), (true, true)) *)
+(*       1 ctx *)
+(*   in *)
   let hook cst = 
     let inst = 
       { is_class = k;