val require_library : string -> unit
val subtac_fixpoint : 'a -> 'b -> unit
val subtac : Util.loc * Vernacexpr.vernac_expr -> unit