Add a flag to control betaiota reduction during unification to maintain backward compatibility.

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

1 files changed, 34 insertions, 28 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 8d7581179b..e70f65308d 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -283,36 +283,42 @@ let named_of_rel_context l =
 let string_of_global r =
  string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r)
 
-let rec declare_subclasses gr (rels, (tc, args)) =
-  let projs = list_map_filter 
-    (fun (n, b, proj) ->
-       if b then Option.map (fun p -> Nameops.out_name n, mkConst p) proj
-       else None) tc.cl_projs 
-  in
-  let instapp = appvectc (constr_of_global gr)
-    (Termops.extended_rel_vect 0 rels)
-  in
-  let projargs = 
-    Array.of_list (args @ [instapp])
-  in
-  let declare_proj (n, p) =
-    let ce = {
-      const_entry_body   = it_mkLambda_or_LetIn (mkApp (p, projargs)) rels;
-      const_entry_type   = None;
-      const_entry_opaque = false }
+let declare_subclasses gr cl =
+  let rec build_subclasses c (rels, (tc, args)) =
+    let projs = list_map_filter 
+      (fun (n, b, proj) ->
+	 if b then Option.map (fun p -> Nameops.out_name n, mkConst p) proj
+	 else None) tc.cl_projs 
     in
-    let cst = Declare.declare_constant ~internal:Declare.KernelSilent 
-      (Nameops.add_suffix (Nameops.add_suffix (id_of_string (string_of_global gr)) "_") 
-	 (string_of_id n))
-      (DefinitionEntry ce, IsAssumption Logical)
+    let instapp = appvectc (constr_of_global gr)
+      (Termops.extended_rel_vect 0 rels)
     in
-    let ty = Typeops.type_of_constant (Global.env ()) cst in
-      match class_of_constr ty with
-      | Some (rels, (tc, args) as cl) ->
-	  add_instance (Typeclasses.new_instance tc None false (ConstRef cst));
-	  declare_subclasses (ConstRef cst) cl
-      | None -> ()
-  in List.iter declare_proj projs
+    let projargs = 
+      Array.of_list (args @ [instapp])
+    in
+    let declare_proj (n, p) =
+      let body = it_mkLambda_or_LetIn (mkApp (p, projargs)) rels in
+	(*     let ce = { *)
+	(*       const_entry_body   = ; *)
+(*       const_entry_type   = None; *)
+(*       const_entry_opaque = false } *)
+(*     in *)
+(*     let cst = Declare.declare_constant ~internal:Declare.KernelSilent  *)
+(*       (Nameops.add_suffix (Nameops.add_suffix (id_of_string (string_of_global gr)) "_")  *)
+(* 	 (string_of_id n)) *)
+(*       (DefinitionEntry ce, IsAssumption Logical) *)
+(*     in *)
+      let ty = Retyping.get_type_of (Global.env ()) Evd.empty body in
+	match class_of_constr ty with
+	| Some (rels, (tc, args) as cl) ->
+	    (* 	  add_instance (Typeclasses.new_instance tc None false (ConstRef cst)); *)
+	    body :: build_subclasses body cl
+	| None -> []
+    in list_map_append declare_proj projs
+  in
+  let hints = build_subclasses (constr_of_global gr) cl in
+  let entry = List.map (fun c -> (None, false, None, c)) hints in
+    Auto.add_hints true (* local *) [typeclasses_db] (Auto.HintsResolveEntry entry)
 
 let context l =
   let env = Global.env() in