G_proofs
val thm_token : Decls.theorem_kind Pcoq.Entry.t
val hint : Vernacexpr.hints_expr Pcoq.Entry.t