package coq-core

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

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.19.0.tar.gz
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b

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.