- 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

1 files changed, 4 insertions, 0 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ca4a82ea6..e3d3d2032 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -782,6 +782,9 @@ let vernac_declare_tactic_definition (local,x,def) =
 let vernac_create_hintdb local id b =
   Auto.create_hint_db local id full_transparent_state b
 
+let vernac_remove_hints local dbs ids =
+  Auto.remove_hints local dbs (List.map Smartlocate.global_with_alias ids)
+
 let vernac_hints local lb h =
   Auto.add_hints local lb (Auto.interp_hints h)
 
@@ -1396,6 +1399,7 @@ let interp c = match c with
   (* Commands *)
   | VernacDeclareTacticDefinition def -> vernac_declare_tactic_definition def
   | VernacCreateHintDb (local,dbname,b) -> vernac_create_hintdb local dbname b
+  | VernacRemoveHints (local,dbnames,ids) -> vernac_remove_hints local dbnames ids
   | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
   | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
   | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l