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
32
33
|
(************************************************************************)
(* * 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_core_plugin", ["plugins";"micromega_core";]) ;
("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"]) ;
("ltac2_ltac1_plugin", ["plugins";"ltac2_ltac1"]) ;
("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"]) ;
]
|
