diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 16 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 8 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 14 |
3 files changed, 19 insertions, 19 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 = diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 2ac4339c16..b303533e48 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -632,8 +632,8 @@ let declare_obligation prg obl body ty uctx = (DefinitionEntry ce,IsProof Property) in if not opaque then - Auto.add_hints false [Id.to_string prg.prg_name] - (Auto.HintsUnfoldEntry [EvalConstRef constant]); + Hints.add_hints false [Id.to_string prg.prg_name] + (Hints.HintsUnfoldEntry [EvalConstRef constant]); definition_message obl.obl_name; { obl with obl_body = if poly then @@ -813,8 +813,8 @@ let rec solve_obligation prg num tac = else DefinedObl cst in if transparent then - Auto.add_hints true [Id.to_string prg.prg_name] - (Auto.HintsUnfoldEntry [EvalConstRef cst]); + Hints.add_hints true [Id.to_string prg.prg_name] + (Hints.HintsUnfoldEntry [EvalConstRef cst]); { obl with obl_body = Some body } in let obls = Array.copy obls in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 63253d54ea..f6bc8bbebe 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -967,15 +967,15 @@ let vernac_declare_tactic_definition locality (x,def) = let vernac_create_hintdb locality id b = let local = make_module_locality locality in - Auto.create_hint_db local id full_transparent_state b + Hints.create_hint_db local id full_transparent_state b let vernac_remove_hints locality dbs ids = let local = make_module_locality locality in - Auto.remove_hints local dbs (List.map Smartlocate.global_with_alias ids) + Hints.remove_hints local dbs (List.map Smartlocate.global_with_alias ids) let vernac_hints locality poly local lb h = let local = enforce_module_locality locality local in - Auto.add_hints local lb (Auto.interp_hints poly h) + Hints.add_hints local lb (Hints.interp_hints poly h) let vernac_syntactic_definition locality lid x local y = Dumpglob.dump_definition lid false "syndef"; @@ -1528,11 +1528,11 @@ let vernac_print = function let univ = if b then Univ.sort_universes univ else univ in msg_notice (Univ.pr_universes univ) | PrintUniverses (b, Some s) -> dump_universes b s - | PrintHint r -> msg_notice (Auto.pr_hint_ref (smart_global r)) - | PrintHintGoal -> msg_notice (Auto.pr_applicable_hint ()) - | PrintHintDbName s -> msg_notice (Auto.pr_hint_db_by_name s) + | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r)) + | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) + | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s) | PrintRewriteHintDbName s -> msg_notice (Autorewrite.print_rewrite_hintdb s) - | PrintHintDb -> msg_notice (Auto.pr_searchtable ()) + | PrintHintDb -> msg_notice (Hints.pr_searchtable ()) | PrintScopes -> msg_notice (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr)) | PrintScope s -> |