val require_library : string -> unit
val subtac : Util.loc * Vernacexpr.vernac_expr -> unit