ltac2_plugin
Tac2entries.Pltac
btauto_plugin
cc_plugin
coq-core.boot
coq-core.clib
coq-core.config
coq-core.engine
coq-core.gramlib
coq-core.interp
coq-core.kernel
coq-core.lib
coq-core.library
coq-core.parsing
coq-core.plugins
coq-core.pretyping
coq-core.printing
coq-core.proofs
coq-core.stm
coq-core.sysinit
coq-core.tactics
coq-core.top_printers
coq-core.toplevel
coq-core.vernac
coq-core.vm
coqide-server.core
coqide-server.protocol
derive_plugin
extraction_plugin
firstorder_plugin
funind_plugin
ltac_plugin
micromega_plugin
nsatz_plugin
number_string_notation_plugin
ring_plugin
rtauto_plugin
ssreflect_plugin
ssrmatching_plugin
tauto_plugin
tuto0_plugin
tuto1_plugin
tuto2_plugin
tuto3_plugin
zify_plugin
val ltac2_expr : Tac2expr.raw_tacexpr Pcoq.Entry.t
val tac2expr_in_env : (Names.Id.t CAst.t list * Tac2expr.raw_tacexpr) Pcoq.Entry.t
Quoted entries. To be used for complex notations.
val q_ident : Names.Id.t CAst.t Tac2qexpr.or_anti Pcoq.Entry.t
val q_bindings : Tac2qexpr.bindings Pcoq.Entry.t
val q_with_bindings : Tac2qexpr.bindings Pcoq.Entry.t
val q_intropattern : Tac2qexpr.intro_pattern Pcoq.Entry.t
val q_intropatterns : Tac2qexpr.intro_pattern list CAst.t Pcoq.Entry.t
val q_destruction_arg : Tac2qexpr.destruction_arg Pcoq.Entry.t
val q_induction_clause : Tac2qexpr.induction_clause Pcoq.Entry.t
val q_conversion : Tac2qexpr.conversion Pcoq.Entry.t
val q_rewriting : Tac2qexpr.rewriting Pcoq.Entry.t
val q_clause : Tac2qexpr.clause Pcoq.Entry.t
val q_dispatch : Tac2qexpr.dispatch Pcoq.Entry.t
val q_occurrences : Tac2qexpr.occurrences Pcoq.Entry.t
val q_reference : Tac2qexpr.reference Tac2qexpr.or_anti Pcoq.Entry.t
val q_strategy_flag : Tac2qexpr.strategy_flag Pcoq.Entry.t
val q_constr_matching : Tac2qexpr.constr_matching Pcoq.Entry.t
val q_goal_matching : Tac2qexpr.goal_matching Pcoq.Entry.t
val q_hintdb : Tac2qexpr.hintdb Pcoq.Entry.t
val q_move_location : Tac2qexpr.move_location Pcoq.Entry.t
val q_pose : Tac2qexpr.pose Pcoq.Entry.t
val q_assert : Tac2qexpr.assertion Pcoq.Entry.t