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