package coq-core

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

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.19.1.tar.gz
md5=13d2793fc6413aac5168822313e4864e
sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42

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.