Module `G_proofs`

module C = Constr

val thm_token : Decls.theorem_kind Pcoq.Entry.t
val hint : Vernacexpr.hints_expr Pcoq.Entry.t
val warn_deprecated_focus : ?⁠loc:Loc.t -> unit -> unit
val warn_deprecated_focus_n : int -> ?⁠loc:Loc.t -> unit -> unit
val warn_deprecated_unfocus : ?⁠loc:Loc.t -> unit -> unit