Up – Package index » rocq-runtime » Sources » cc_plugin » cc_plugin.ml

Source file `cc_plugin.ml`

rocq-runtime
- README
- Library btauto_plugin
  - Btauto_plugin
- Library byte_config
  - Coq_byte_config
- Library cc_core_plugin
  - Cc_core_plugin
- Library cc_plugin
  - Cc_plugin
- Library derive_plugin
  - Derive_plugin
- Library extraction_plugin
  - Extraction_plugin
- Library firstorder_core_plugin
  - Firstorder_core_plugin
- Library firstorder_plugin
  - Firstorder_plugin
- Library funind_plugin
  - Funind_plugin
- Library ltac2_ltac1_plugin
  - Ltac2_ltac1_plugin
- Library ltac2_plugin
  - Ltac2_plugin
- Library ltac_plugin
  - Ltac_plugin
- Library micromega_core_plugin
  - Micromega_core_plugin
- Library micromega_plugin
  - Micromega_plugin
- Library nsatz_core_plugin
  - Nsatz_core_plugin
- Library nsatz_plugin
  - Nsatz_plugin
- Library number_string_notation_plugin
  - Number_string_notation_plugin
- Library ring_plugin
  - Ring_plugin
- Library rocq-runtime.boot
  - Boot
- Library rocq-runtime.checklib
  - Coq_checklib
- Library rocq-runtime.clib
- Library rocq-runtime.config
  - Coq_config
- Library rocq-runtime.coqargs
  - Coqargs
- Library rocq-runtime.coqdeplib
  - Coqdeplib
- Library rocq-runtime.coqworkmgrapi
  - CoqworkmgrApi
- Library rocq-runtime.debugger_support
  - Debugger_support
- Library rocq-runtime.dev
  - Top_printers
  - Vm_printers
- Library rocq-runtime.engine
- Library rocq-runtime.gramlib
  - Gramlib
- Library rocq-runtime.interp
- Library rocq-runtime.kernel
- Library rocq-runtime.lib
- Library rocq-runtime.library
- Library rocq-runtime.parsing
- Library rocq-runtime.perf
  - Perf
- Library rocq-runtime.plugins
- Library rocq-runtime.pretyping
- Library rocq-runtime.printing
- Library rocq-runtime.proofs
- Library rocq-runtime.rocqshim
  - Rocqshim
- Library rocq-runtime.stm
- Library rocq-runtime.sysinit
  - Coqinit
  - Coqloadpath
- Library rocq-runtime.tactics
- Library rocq-runtime.toplevel
- Library rocq-runtime.vernac
- Library rocq-runtime.vm
  - Coqrun
- Library rtauto_plugin
  - Rtauto_plugin
- Library ssreflect_plugin
  - Ssreflect_plugin
- Library ssrmatching_plugin
  - Ssrmatching_plugin
- Library tauto_plugin
  - Tauto_plugin
- Library tuto0_plugin
  - Tuto0_plugin
- Library tuto1_plugin
  - Tuto1_plugin
- Library tuto2_plugin
  - Tuto2_plugin
- Library tuto3_plugin
  - Tuto3_plugin
- Library zify_plugin
  - Zify_plugin
- Sources
  - btauto_plugin
  - byte_config
    - coq_byte_config.ml
  - cc_core_plugin
  - cc_plugin
    - cc_plugin.ml
    - g_congruence.ml
  - derive_plugin
  - extraction_plugin
  - firstorder_core_plugin
  - firstorder_plugin
    - firstorder_plugin.ml
    - g_ground.ml
  - funind_plugin
  - ltac2_ltac1_plugin
  - ltac2_plugin
  - ltac_plugin
  - micromega_core_plugin
  - micromega_plugin
  - nsatz_core_plugin
  - nsatz_plugin
    - g_nsatz.ml
    - nsatz_plugin.ml
  - number_string_notation_plugin
  - ring_plugin
  - rocq-runtime.boot
  - rocq-runtime.checklib
  - rocq-runtime.clib
  - rocq-runtime.config
    - coq_config.ml
  - rocq-runtime.coqargs
    - coqargs.ml
  - rocq-runtime.coqdeplib
  - rocq-runtime.coqworkmgrapi
    - coqworkmgrApi.ml
  - rocq-runtime.debugger_support
    - debugger_support.ml
  - rocq-runtime.dev
    - top_printers.ml
    - vm_printers.ml
  - rocq-runtime.engine
  - rocq-runtime.gramlib
  - rocq-runtime.interp
  - rocq-runtime.kernel
  - rocq-runtime.lib
  - rocq-runtime.library
  - rocq-runtime.parsing
  - rocq-runtime.perf
    - perf.ml
  - rocq-runtime.pretyping
  - rocq-runtime.printing
  - rocq-runtime.proofs
  - rocq-runtime.rocqshim
    - rocqshim.ml
  - rocq-runtime.stm
  - rocq-runtime.sysinit
    - coqinit.ml
    - coqloadpath.ml
  - rocq-runtime.tactics
  - rocq-runtime.toplevel
  - rocq-runtime.vernac
  - rocq-runtime.vm
    - coqrun.ml
  - rtauto_plugin
  - ssreflect_plugin
  - ssrmatching_plugin
  - tauto_plugin
    - tauto.ml
    - tauto_plugin.ml
  - tuto0_plugin
  - tuto1_plugin
  - tuto2_plugin
  - tuto3_plugin
  - zify_plugin

1
2
3
4
(* generated by dune *)

(** @canonical Cc_plugin.G_congruence *)
module G_congruence = Cc_plugin__G_congruence