ssreflect_plugin
Ssreflect_plugin.Ssrprinters
btauto_plugin
byte_config
cc_core_plugin
cc_plugin
derive_plugin
extraction_plugin
firstorder_core_plugin
firstorder_plugin
funind_plugin
ltac2_ltac1_plugin
ltac2_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
ssrmatching_plugin
tauto_plugin
tuto0_plugin
tuto1_plugin
tuto2_plugin
tuto3_plugin
zify_plugin
val pr_spc : unit -> Pp.t
val pr_bar : unit -> Pp.t
val pr_list : (unit -> Pp.t) -> ('a -> Pp.t) -> 'a list -> Pp.t
val pp_concat : Pp.t -> ?sep:Pp.t -> Pp.t list -> Pp.t
val pr_clear : (unit -> Pp.t) -> Ssrast.ssrclear -> Pp.t
val pr_clear_ne : Ssrast.ssrclear -> Pp.t
val pr_dir : Ssrast.ssrdir -> Pp.t
val pr_simpl : Ssrast.ssrsimpl -> Pp.t
val pr_term : (Ssrast.ssrtermkind * (Glob_term.glob_constr * Constrexpr.constr_expr option)) -> Pp.t
val pr_ast_closure_term : Ssrast.ast_closure_term -> Pp.t
val pr_view2 : Ssrast.ast_closure_term list -> Pp.t
val pr_ipat : Ssrast.ssripat -> Pp.t
val pr_ipats : Ssrast.ssripats -> Pp.t
val pr_iorpat : Ssrast.ssripatss -> Pp.t
val pr_block : Ssrast.id_block -> Pp.t
val pr_hyp : Ssrast.ssrhyp -> Pp.t
val pr_hyps : Ssrast.ssrhyps -> Pp.t
val prl_constr_expr : Constrexpr.constr_expr -> Pp.t
val prl_glob_constr : Glob_term.glob_constr -> Pp.t
val pr_guarded : (string -> int -> bool) -> ('a -> Pp.t) -> 'a -> Pp.t
val pr_occ : Ssrast.ssrocc -> Pp.t
val debug_ssr : CDebug.t