aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--vernac/command.ml5
-rw-r--r--vernac/command.mli5
2 files changed, 0 insertions, 10 deletions
diff --git a/vernac/command.ml b/vernac/command.ml
index 406477356..68fa8ab88 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -167,10 +167,6 @@ let declare_global_definition ident ce local k pl imps =
let () = definition_message ident in
gr
-let declare_definition_hook = ref ignore
-let set_declare_definition_hook = (:=) declare_definition_hook
-let get_declare_definition_hook () = !declare_definition_hook
-
let warn_definition_not_visible =
CWarnings.create ~name:"definition-not-visible" ~category:"implicits"
(fun ident ->
@@ -179,7 +175,6 @@ let warn_definition_not_visible =
let declare_definition ident (local, p, k) ce pl imps hook =
let fix_exn = Future.fix_exn_of ce.const_entry_body in
- let () = !declare_definition_hook ce in
let r = match local with
| Discharge when Lib.sections_are_opened () ->
let c = SectionLocalDef ce in
diff --git a/vernac/command.mli b/vernac/command.mli
index a636bc03c..f7d90ce60 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -23,11 +23,6 @@ val do_universe : polymorphic -> Id.t Loc.located list -> unit
val do_constraint : polymorphic ->
(Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> unit
-(** {6 Hooks for Pcoq} *)
-
-val set_declare_definition_hook : (Safe_typing.private_constants definition_entry -> unit) -> unit
-val get_declare_definition_hook : unit -> (Safe_typing.private_constants definition_entry -> unit)
-
(** {6 Definitions/Let} *)
val interp_definition :