Change Hint Resolve, Immediate to take a global reference as argument

instead of a general constr: this is the most common case and does
not loose generality (one can simply define constrs before Hint Resolving
them). Benefits:
- Natural semantics for typeclasses, not class resolution needed at
Hint Resolve time, meaning less trouble for users as well.
- Ability to [Hint Remove] any hint so declared.
- Simplifies the implementation as well.


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

2 files changed, 24 insertions, 6 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 2749538c0..95fdcdfe6 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -39,6 +39,11 @@ let classes_transparent_state_ref = ref (fun () -> assert false)
 let register_classes_transparent_state = (:=) classes_transparent_state_ref
 let classes_transparent_state () = !classes_transparent_state_ref ()
 
+
+let declare_definition_ref = ref (fun ?internal ?opaque ?kind id ?types constr -> assert false)
+let register_declare_definition =
+  (:=) declare_definition_ref
+
 let solve_instanciation_problem = ref (fun _ _ _ -> assert false)
 
 let resolve_one_typeclass env evm t =
@@ -238,6 +243,12 @@ let check_instance env sigma c =
   with _ -> false
 
 let build_subclasses ~check env sigma glob pri =
+  let id = Nametab.basename_of_global glob in
+  let next_id = 
+    let i = ref (-1) in 
+      (fun () -> incr i;
+        Nameops.add_suffix id ("_subinstance_" ^ string_of_int !i))
+  in
   let rec aux pri c =
     let ty = Evarutil.nf_evar sigma (Retyping.get_type_of env sigma c) in
       match class_of_constr ty with
@@ -261,10 +272,13 @@ let build_subclasses ~check env sigma glob pri =
 		   | Some p, None -> Some (p + 1)
 		   | _, _ -> None
 		 in
-		   Some (ConstRef proj, pri, body)) tc.cl_projs 
+		 let c = !declare_definition_ref ~internal:true
+		   ~kind:Decl_kinds.Instance (next_id ()) body 
+		 in
+		   Some (ConstRef proj, pri, ConstRef c)) tc.cl_projs 
 	in
 	let declare_proj hints (cref, pri, body) =
-	  let rest = aux pri body in
+	  let rest = aux pri (constr_of_global body) in
 	    hints @ (pri, body) :: rest
 	in List.fold_left declare_proj [] projs 
   in aux pri (constr_of_global glob)
@@ -313,7 +327,7 @@ let discharge_instance (_, (action, inst)) =
 let is_local i = i.is_global = -1
 
 let add_instance check inst =
-  add_instance_hint (constr_of_global inst.is_impl) (is_local inst) inst.is_pri;
+  add_instance_hint inst.is_impl (is_local inst) inst.is_pri;
   List.iter (fun (pri, c) -> add_instance_hint c (is_local inst) pri) 
     (build_subclasses ~check:(check && not (isVarRef inst.is_impl))
        (Global.env ()) Evd.empty inst.is_impl inst.is_pri)
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 039aeb1e6..729cbb2ad 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -103,9 +103,13 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u
 val register_classes_transparent_state : (unit -> transparent_state) -> unit
 val classes_transparent_state : unit -> transparent_state
 
-val register_add_instance_hint : (constr -> bool (* local? *) -> int option -> unit) -> unit
+val register_declare_definition : (?internal:bool -> ?opaque:bool -> ?kind:definition_object_kind -> identifier -> ?types:constr -> constr -> constant) -> unit
+
+
+val register_add_instance_hint : 
+  (global_reference -> bool (* local? *) -> int option -> unit) -> unit
 val register_remove_instance_hint : (global_reference -> unit) -> unit
-val add_instance_hint : constr -> bool -> int option -> unit
+val add_instance_hint : global_reference -> bool -> int option -> unit
 val remove_instance_hint : global_reference -> unit
 
 val solve_instanciations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> evar_map) ref
@@ -119,4 +123,4 @@ val declare_instance : int option -> bool -> global_reference -> unit
     subinstances and add only the missing ones. *)
 
 val build_subclasses : check:bool -> env -> evar_map -> global_reference -> int option (* priority *) ->
-  (int option * constr) list
+  (int option * global_reference) list