package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val __coq_plugin_name : string
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_name : 'a -> 'b -> 'c -> Class_tactics.search_strategy -> Pp.t
val pr_search_strategy : 'a -> 'b -> 'c -> Class_tactics.search_strategy option -> Pp.t
val eauto_search_strategy_name : Class_tactics.search_strategy Pcoq.Entry.t
val eauto_search_strategy : Class_tactics.search_strategy option Pcoq.Entry.t

TODO: DEPRECATE

val eq_constr_mod_evars : Evd.evar_map -> EConstr.t -> EConstr.t -> bool
val progress_evars : unit Proofview.tactic -> unit Proofview.tactic