package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

coq 8.11.1

Libraries

This package provides the following libraries (via ocamlobjinfo):

coq.config

Documentation:

coq.clib

Documentation:

coq.lib

Documentation:

coq.vm

Documentation:

    coq.kernel

    Documentation:

    coq.library

    Documentation:

    coq.engine

    Documentation:

    coq.pretyping

    Documentation:

    coq.interp

    Documentation:

    coq.proofs

    Documentation:

    coq.gramlib

    Documentation:

    coq.parsing

    Documentation:

    coq.printing

    Documentation:

    coq.tactics

    Documentation:

    coq.vernac

    Documentation:

    coq.stm

    Documentation:

    coq.toplevel

    Documentation:

    coq.idetop

    Documentation:

      coq.ide

      Documentation:

        coq.plugins.ltac

        Documentation:

          coq.plugins.tauto

          Documentation:

            coq.plugins.omega

            Documentation:

              coq.plugins.micromega

              Documentation:

                coq.plugins.zify

                Documentation:

                  coq.plugins.setoid_ring

                  Documentation:

                    coq.plugins.extraction

                    Documentation:

                      coq.plugins.cc

                      Documentation:

                        coq.plugins.firstorder

                        Documentation:

                          coq.plugins.rtauto

                          Documentation:

                            coq.plugins.btauto

                            Documentation:

                              coq.plugins.funind

                              Documentation:

                                coq.plugins.nsatz

                                Documentation:

                                  coq.plugins.rsyntax

                                  Documentation:

                                    coq.plugins.int63syntax

                                    Documentation:

                                      coq.plugins.string_notation

                                      Documentation:

                                        coq.plugins.derive

                                        Documentation:

                                          coq.plugins.ssrmatching

                                          Documentation:

                                            coq.plugins.ssreflect

                                            Documentation:

                                              coq.plugins.ltac2

                                              Documentation: