G_proofs (p.coq-core.8.17.1.doc.coq-core.vernac.G

module C = Constr

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