Add a flag for restricting resolution of typeclasses to

matching (i.e. no instanciation of the goal evars).
Classes defined when [Set Typeclasses Strict Resolution] is on
use the restricted resolution for all their instances (except
for Hint Extern's).

2 files changed, 18 insertions, 7 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index b9c2bd1bb3..a3bd06ed5d 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -52,6 +52,8 @@ type typeclass = {
 
   (* The method implementaions as projections. *)
   cl_projs : (Name.t * (direction * int option) option * constant option) list;
+  
+  cl_strict : bool;
 }
 
 type typeclasses = typeclass Refmap.t
@@ -174,7 +176,8 @@ let subst_class (subst,cl) =
   { cl_impl = do_subst_gr cl.cl_impl;
     cl_context = do_subst_context cl.cl_context;
     cl_props = do_subst_ctx cl.cl_props;
-    cl_projs = do_subst_projs cl.cl_projs; }
+    cl_projs = do_subst_projs cl.cl_projs;
+    cl_strict = cl.cl_strict }
 
 let discharge_class (_,cl) =
   let repl = Lib.replacement_context () in
@@ -214,10 +217,13 @@ let discharge_class (_,cl) =
     let ctx, subst = rel_of_variable_context ctx in
     let context = discharge_context ctx subst cl.cl_context in
     let props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props in
-    { cl_impl = cl_impl';
-      cl_context = context;
-      cl_props = props;
-      cl_projs = List.smartmap (fun (x, y, z) -> x, y, Option.smartmap Lib.discharge_con z) cl.cl_projs }
+    let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in
+      { cl_impl = cl_impl';
+	cl_context = context;
+	cl_props = props;
+	cl_projs = List.smartmap discharge_proj cl.cl_projs;
+	cl_strict = cl.cl_strict;
+      }
 
 let rebuild_class cl = 
   try 
@@ -411,7 +417,8 @@ let add_constant_class cst =
     { cl_impl = ConstRef cst;
       cl_context = (List.map (const None) ctx, ctx);
       cl_props = [(Anonymous, None, arity)];
-      cl_projs = []
+      cl_projs = [];
+      cl_strict = false;
     }
   in add_class tc;
     set_typeclass_transparency (EvalConstRef cst) false false
@@ -429,7 +436,8 @@ let add_inductive_class ind =
       { cl_impl = IndRef ind;
 	cl_context = List.map (const None) ctx, ctx;
 	cl_props = [Anonymous, None, ty];
-	cl_projs = [] }
+	cl_projs = [];
+	cl_strict = false }
   in add_class k
       
 (*
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 7c3d2be09b..b1f816e651 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -34,6 +34,9 @@ type typeclass = {
       no name is provided. The [int option option] indicates subclasses whose hint has
       the given priority. *)
   cl_projs : (Name.t * (direction * int option) option * constant option) list;
+
+  (** Whether we use matching or full unification during resolution *)
+  cl_strict : bool; 
 }
 
 type instance