package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c

doc/src/coq-core.lib/core_plugins_findlib_compat.ml.html

Source file core_plugins_findlib_compat.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

let legacy_to_findlib = [
  ("btauto_plugin",                 ["plugins";"btauto"]) ;
  ("derive_plugin",                 ["plugins";"derive"]) ;
  ("firstorder_plugin",             ["plugins";"firstorder"]) ;
  ("ltac_plugin",                   ["plugins";"ltac"]) ;
  ("micromega_plugin",              ["plugins";"micromega"]) ;
  ("ring_plugin",                   ["plugins";"ring"]) ;
  ("ssr_plugin",                    ["plugins";"ssr"]) ;
  ("syntax_plugin",                 ["plugins";"syntax"]) ;
  ("cc_plugin",                     ["plugins";"cc"]) ;
  ("extraction_plugin",             ["plugins";"extraction"]) ;
  ("funind_plugin",                 ["plugins";"funind"]) ;
  ("ltac2_plugin",                  ["plugins";"ltac2"]) ;
  ("nsatz_plugin",                  ["plugins";"nsatz"]) ;
  ("rtauto_plugin",                 ["plugins";"rtauto"]) ;
  ("ssrmatching_plugin",            ["plugins";"ssrmatching"]) ;
  ("ssreflect_plugin",              ["plugins";"ssreflect"]) ;
  ("number_string_notation_plugin", ["plugins";"number_string_notation"]) ;
  ("zify_plugin",                   ["plugins";"zify"]) ;
  ("tauto_plugin",                  ["plugins";"tauto"]) ;
]
OCaml

Innovation. Community. Security.