G_proofs (u.75d6a066538fb738038ab1b402df0edb.coq.8.14.1.doc.coq-core.vernac.G

Sourceval thm_token : Decls.theorem_kind Pcoq.Entry.t

Sourceval hint : Vernacexpr.hints_expr Pcoq.Entry.t

Sourceval warn_deprecated_focus : ?loc:Loc.t -> unit -> unit

Sourceval warn_deprecated_focus_n : int -> ?loc:Loc.t -> unit -> unit

Sourceval warn_deprecated_unfocus : ?loc:Loc.t -> unit -> unit