Up – Package index » coq-core » Sources » tauto_plugin » tauto_plugin.ml

Source file `tauto_plugin.ml`

coq-core
- README
- Library btauto_plugin
  - Btauto_plugin
- Library byte_config
  - Coq_byte_config
- Library cc_plugin
  - Cc_plugin
- Library coq-core.boot
  - Boot
- Library coq-core.checklib
  - Coq_checklib
- Library coq-core.clib
- Library coq-core.config
  - Coq_config
- Library coq-core.coqworkmgrapi
  - CoqworkmgrApi
- Library coq-core.debugger_support
  - Debugger_support
- Library coq-core.dev
  - Top_printers
  - Vm_printers
- Library coq-core.engine
- Library coq-core.gramlib
  - Gramlib
- Library coq-core.interp
- Library coq-core.kernel
- Library coq-core.lib
- Library coq-core.library
- Library coq-core.parsing
- Library coq-core.perf
  - Perf
- Library coq-core.plugins
- Library coq-core.pretyping
- Library coq-core.printing
- Library coq-core.proofs
- Library coq-core.stm
- Library coq-core.sysinit
- Library coq-core.tactics
- Library coq-core.toplevel
- Library coq-core.vernac
- Library coq-core.vm
  - Coqrun
- Library derive_plugin
  - Derive_plugin
- Library extraction_plugin
  - Extraction_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_plugin
  - Nsatz_plugin
- Library number_string_notation_plugin
  - Number_string_notation_plugin
- Library ring_plugin
  - Ring_plugin
- 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_plugin
  - coq-core.boot
  - coq-core.checklib
  - coq-core.clib
  - coq-core.config
    - coq_config.ml
  - coq-core.coqworkmgrapi
    - coqworkmgrApi.ml
  - coq-core.debugger_support
    - debugger_support.ml
  - coq-core.dev
    - top_printers.ml
    - vm_printers.ml
  - coq-core.engine
  - coq-core.gramlib
  - coq-core.interp
  - coq-core.kernel
  - coq-core.lib
  - coq-core.library
  - coq-core.parsing
  - coq-core.perf
    - perf.ml
  - coq-core.pretyping
  - coq-core.printing
  - coq-core.proofs
  - coq-core.stm
  - coq-core.sysinit
  - coq-core.tactics
  - coq-core.toplevel
  - coq-core.vernac
  - coq-core.vm
    - coqrun.ml
  - derive_plugin
  - extraction_plugin
  - firstorder_plugin
  - funind_plugin
  - ltac2_ltac1_plugin
  - ltac2_plugin
  - ltac_plugin
  - micromega_core_plugin
  - micromega_plugin
  - nsatz_plugin
  - number_string_notation_plugin
  - ring_plugin
  - 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 Tauto_plugin.Tauto *)
module Tauto = Tauto_plugin__Tauto