From 9eeb0905d1d6f2c9e7b9be83660335838d2c1295 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 27 Mar 2008 00:57:38 +0000
Subject: 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
---
 contrib/subtac/subtac_classes.ml | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

(limited to 'contrib')

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;
-- 
cgit v1.2.3