G_proofsmodule C = Constrval thm_token : Decls.theorem_kind Pcoq.Entry.tval hint : Vernacexpr.hints_expr Pcoq.Entry.tval warn_deprecated_focus : ?loc:Loc.t -> unit -> unitval warn_deprecated_focus_n : int -> ?loc:Loc.t -> unit -> unitval warn_deprecated_unfocus : ?loc:Loc.t -> unit -> unit