- Fix treatment of globality flag for typeclass instance hints (they

  were all declared as global).
- Add possibility to remove hints (Resolve or Immediate only) based on
  the name of the lemma.


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

2 files changed, 54 insertions, 19 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 84815e0988..12cccdf0c3 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -22,11 +22,16 @@ open Libobject
 (*i*)
 
 
-let add_instance_hint_ref = ref (fun id pri -> assert false)
+let add_instance_hint_ref = ref (fun id local pri -> assert false)
 let register_add_instance_hint =
   (:=) add_instance_hint_ref
 let add_instance_hint id = !add_instance_hint_ref id
 
+let remove_instance_hint_ref = ref (fun id -> assert false)
+let register_remove_instance_hint =
+  (:=) remove_instance_hint_ref
+let remove_instance_hint id = !remove_instance_hint_ref id
+
 let set_typeclass_transparency_ref = ref (fun id pri -> assert false)
 let register_set_typeclass_transparency =
   (:=) set_typeclass_transparency_ref
@@ -212,50 +217,77 @@ let add_class cl =
  * instances persistent object
  *)
 
-let load_instance (_,inst) = 
+type instance_action = 
+  | AddInstance
+  | RemoveInstance
+
+let load_instance inst = 
   let insts = 
     try Gmap.find inst.is_class !instances 
     with Not_found -> Gmap.empty in
   let insts = Gmap.add inst.is_impl inst insts in
   instances := Gmap.add inst.is_class insts !instances
 
-let cache_instance = load_instance
+let remove_instance inst =
+  let insts = 
+    try Gmap.find inst.is_class !instances 
+    with Not_found -> assert false in
+  let insts = Gmap.remove inst.is_impl insts in
+  instances := Gmap.add inst.is_class insts !instances
+
+let cache_instance (_, (action, i)) =
+  match action with 
+  | AddInstance -> load_instance i
+  | RemoveInstance -> remove_instance i      
 
-let subst_instance (subst,inst) = 
+let subst_instance (subst, (action, inst)) = action,
   { inst with 
       is_class = fst (subst_global subst inst.is_class);
       is_impl = fst (subst_global subst inst.is_impl) }
 
-let discharge_instance (_,inst) =
+let discharge_instance (_, (action, inst)) =
   if inst.is_global <= 0 then None
-  else Some 
+  else Some (action,
     { inst with 
       is_global = pred inst.is_global;
       is_class = Lib.discharge_global inst.is_class;
-      is_impl = Lib.discharge_global inst.is_impl }
+      is_impl = Lib.discharge_global inst.is_impl })
     
-let rebuild_instance inst =
-  add_instance_hint inst.is_impl inst.is_pri;
-  inst
 
-let classify_instance inst =
-  if inst.is_global = -1 then Dispose
-  else Substitute inst
+let is_local i = i.is_global = -1
+
+let rebuild_instance (action, inst) =
+  if action = AddInstance then
+    add_instance_hint inst.is_impl (is_local inst) inst.is_pri;
+  (action, inst)
+
+let classify_instance (action, inst) =
+  if is_local inst then Dispose
+  else Substitute (action, inst)
+
+let load_instance (_, (action, inst) as ai) =
+  cache_instance ai;
+  if action = AddInstance then
+    add_instance_hint inst.is_impl (is_local inst) inst.is_pri
 
 let instance_input =
   declare_object
     { (default_object "type classes instances state") with
       cache_function = cache_instance;
-      load_function = (fun _ -> load_instance);
-      open_function = (fun _ -> load_instance);
+      load_function = (fun _ x -> cache_instance x);
+      open_function = (fun _ x -> cache_instance x);
       classify_function = classify_instance;
       discharge_function = discharge_instance;
       rebuild_function = rebuild_instance;
       subst_function = subst_instance }
 
 let add_instance i =
-  Lib.add_anonymous_leaf (instance_input i);
-  add_instance_hint i.is_impl i.is_pri
+  Lib.add_anonymous_leaf (instance_input (AddInstance, i));
+  add_instance_hint i.is_impl (is_local i) i.is_pri
+
+let remove_instance i =
+  Lib.add_anonymous_leaf (instance_input (RemoveInstance, i));
+  remove_instance_hint i.is_impl
 
 open Declarations
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 800deefda4..3fa1981a3c 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -52,6 +52,7 @@ val add_inductive_class : inductive -> unit
 
 val new_instance : typeclass -> int option -> bool -> global_reference -> instance
 val add_instance : instance -> unit
+val remove_instance : instance -> unit
 
 val class_info : global_reference -> typeclass (** raises a UserError if not a class *)
 
@@ -89,8 +90,10 @@ val resolve_one_typeclass : env -> evar_map -> types -> open_constr
 val register_set_typeclass_transparency : (evaluable_global_reference -> bool -> unit) -> unit
 val set_typeclass_transparency : evaluable_global_reference -> bool -> unit
 
-val register_add_instance_hint : (global_reference -> int option -> unit) -> unit
-val add_instance_hint : global_reference -> int option -> 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 : global_reference -> bool -> int option -> unit
+val remove_instance_hint : global_reference -> unit
 
 val solve_instanciations_problem : (env -> evar_map -> bool -> bool -> bool -> evar_map) ref
 val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref