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