diff options
| author | Hugo Herbelin | 2014-10-07 17:26:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-07 18:40:36 +0200 |
| commit | 38b34dfffcceab7fa7d5ba43c84e414d24cebe43 (patch) | |
| tree | c5449cf9c02c97586bf8a8edaa52d05d876d3e94 /toplevel/classes.ml | |
| parent | 2313bde0116a5916912bebbaca77d291f7b2760a (diff) | |
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
being able to export hints without tactics, vm, etc. to come with.
Some functions moved to the new proof engine.
Diffstat (limited to 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 8f36fc79fe..4d23a41818 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -28,22 +28,22 @@ open Entries let typeclasses_db = "typeclass_instances" let set_typeclass_transparency c local b = - Auto.add_hints local [typeclasses_db] - (Auto.HintsTransparencyEntry ([c], b)) + Hints.add_hints local [typeclasses_db] + (Hints.HintsTransparencyEntry ([c], b)) let _ = Hook.set Typeclasses.add_instance_hint_hook (fun inst path local pri poly -> - let inst' = match inst with IsConstr c -> Auto.IsConstr (c, Univ.ContextSet.empty) - | IsGlobal gr -> Auto.IsGlobRef gr + let inst' = match inst with IsConstr c -> Hints.IsConstr (c, Univ.ContextSet.empty) + | IsGlobal gr -> Hints.IsGlobRef gr in Flags.silently (fun () -> - Auto.add_hints local [typeclasses_db] - (Auto.HintsResolveEntry - [pri, poly, false, Auto.PathHints path, inst'])) ()); + Hints.add_hints local [typeclasses_db] + (Hints.HintsResolveEntry + [pri, poly, false, Hints.PathHints path, inst'])) ()); Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency; Hook.set Typeclasses.classes_transparent_state_hook - (fun () -> Auto.Hint_db.transparent_state (Auto.searchtable_map typeclasses_db)) + (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db)) (** TODO: add subinstances *) let existing_instance glob g pri = |