From de46c3f782dd618e947e7270cd398abf1fd514c2 Mon Sep 17 00:00:00 2001 From: msozeau Date: Sat, 8 Dec 2012 21:39:19 +0000 Subject: Finish patch for Hint Resolve, stopping to generate new constant names for hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16052 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/classes.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'toplevel') diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 43caf3fa3..618ec2bc0 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -24,6 +24,7 @@ open Constrexpr open Decl_kinds open Entries +open Misctypes let typeclasses_db = "typeclass_instances" @@ -33,12 +34,11 @@ let set_typeclass_transparency c local b = let _ = Typeclasses.register_add_instance_hint - (fun inst local pri -> - let path = try Auto.PathHints [inst] with _ -> Auto.PathAny in + (fun inst path local pri -> Flags.silently (fun () -> Auto.add_hints local [typeclasses_db] (Auto.HintsResolveEntry - [pri, false, path, inst])) ()); + [pri, false, Auto.PathHints path, inst])) ()); Typeclasses.register_set_typeclass_transparency set_typeclass_transparency; Typeclasses.register_classes_transparent_state (fun () -> Auto.Hint_db.transparent_state (Auto.searchtable_map typeclasses_db)) -- cgit v1.2.3