- val __coq_plugin_name : string
- val set_transparency : Libnames.qualid list -> bool -> unit
- val pr_debug : 'a -> 'b -> 'c -> bool -> Pp.t
- val wit_debug : (bool, bool, bool) Genarg.genarg_type
- val debug : bool Pcoq.Entry.t
- val pr_search_strategy : 'a -> 'b -> 'c -> Class_tactics.search_strategy option -> Pp.t
- val wit_eauto_search_strategy : (Class_tactics.search_strategy option, Class_tactics.search_strategy option, Class_tactics.search_strategy option) Genarg.genarg_type
- val eauto_search_strategy : Class_tactics.search_strategy option Pcoq.Entry.t
- val deprecated_autoapply_using : ?loc:Loc.t -> unit -> unit
- val eq_constr_mod_evars : Evd.evar_map -> EConstr.t -> EConstr.t -> bool
- val progress_evars : unit Proofview.tactic -> unit Proofview.tactic