From 638b820bf3e150ff295337189c505df351ca7e32 Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Tue, 16 Jan 2018 09:50:03 +0100 Subject: Add plugins to META.coq --- META.coq | 285 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 285 insertions(+) diff --git a/META.coq b/META.coq index f7998db8e..9d0e948e6 100644 --- a/META.coq +++ b/META.coq @@ -293,3 +293,288 @@ package "ide" ( archive(native) = "ide.cmxa" ) + +package "plugins" ( + + description = "Coq built-in plugins" + version = "8.7" + + requires = "" + directory = "plugins" + + package "tauto" ( + + description = "Coq tauto plugin" + version = "8.7" + + requires = "coq.ltac" + directory = "ltac" + + archive(byte) = "tauto_plugin.cmo" + archive(native) = "tauto_plugin.cmx" + ) + + package "omega" ( + + description = "Coq omega plugin" + version = "8.7" + + requires = "coq.ltac" + directory = "omega" + + archive(byte) = "omega_plugin.cmo" + archive(native) = "omega_plugin.cmx" + ) + + package "romega" ( + + description = "Coq romega plugin" + version = "8.7" + + requires = "coq.plugins.omega" + directory = "romega" + + archive(byte) = "romega_plugin.cmo" + archive(native) = "romega_plugin.cmx" + ) + + package "micromega" ( + + description = "Coq micromega plugin" + version = "8.7" + + requires = "num,coq.ltac" + directory = "micromega" + + archive(byte) = "micromega_plugin.cmo" + archive(native) = "micromega_plugin.cmx" + ) + + package "quote" ( + + description = "Coq quote plugin" + version = "8.7" + + requires = "coq.ltac" + directory = "quote" + + archive(byte) = "quote_plugin.cmo" + archive(native) = "quote_plugin.cmx" + ) + + package "newring" ( + + description = "Coq newring plugin" + version = "8.7" + + requires = "coq.plugins.quote" + directory = "setoid_ring" + + archive(byte) = "newring_plugin.cmo" + archive(native) = "newring_plugin.cmx" + ) + + package "fourier" ( + + description = "Coq fourier plugin" + version = "8.7" + + requires = "coq.ltac" + directory = "fourier" + + archive(byte) = "fourier_plugin.cmo" + archive(native) = "fourier_plugin.cmx" + ) + + package "extraction" ( + + description = "Coq extraction plugin" + version = "8.7" + + requires = "coq.ltac" + directory = "extraction" + + archive(byte) = "extraction_plugin.cmo" + archive(native) = "extraction_plugin.cmx" + ) + + package "cc" ( + + description = "Coq cc plugin" + version = "8.7" + + requires = "coq.ltac" + directory = "cc" + + archive(byte) = "cc_plugin.cmo" + archive(native) = "cc_plugin.cmx" + ) + + package "ground" ( + + description = "Coq ground plugin" + version = "8.7" + + requires = "coq.ltac" + directory = "firstorder" + + archive(byte) = "ground_plugin.cmo" + archive(native) = "ground_plugin.cmx" + ) + + package "rtauto" ( + + description = "Coq rtauto plugin" + version = "8.7" + + requires = "coq.ltac" + directory = "rtauto" + + archive(byte) = "rtauto_plugin.cmo" + archive(native) = "rtauto_plugin.cmx" + ) + + package "btauto" ( + + description = "Coq btauto plugin" + version = "8.7" + + requires = "coq.ltac" + directory = "btauto" + + archive(byte) = "btauto_plugin.cmo" + archive(native) = "btauto_plugin.cmx" + ) + + package "recdef" ( + + description = "Coq recdef plugin" + version = "8.7" + + requires = "coq.plugins.extraction" + directory = "funind" + + archive(byte) = "recdef_plugin.cmo" + archive(native) = "recdef_plugin.cmx" + ) + + package "nsatz" ( + + description = "Coq nsatz plugin" + version = "8.7" + + requires = "num,coq.ltac" + directory = "nsatz" + + archive(byte) = "nsatz_plugin.cmo" + archive(native) = "nsatz_plugin.cmx" + ) + + package "natsyntax" ( + + description = "Coq natsyntax plugin" + version = "8.7" + + requires = "" + directory = "syntax" + + archive(byte) = "nat_syntax_plugin.cmo" + archive(native) = "nat_syntax_plugin.cmx" + ) + + package "zsyntax" ( + + description = "Coq zsyntax plugin" + version = "8.7" + + requires = "" + directory = "syntax" + + archive(byte) = "z_syntax_plugin.cmo" + archive(native) = "z_syntax_plugin.cmx" + ) + + package "rsyntax" ( + + description = "Coq rsyntax plugin" + version = "8.7" + + requires = "" + directory = "syntax" + + archive(byte) = "r_syntax_plugin.cmo" + archive(native) = "r_syntax_plugin.cmx" + ) + + package "int31syntax" ( + + description = "Coq int31syntax plugin" + version = "8.7" + + requires = "" + directory = "syntax" + + archive(byte) = "int31_syntax_plugin.cmo" + archive(native) = "int31_syntax_plugin.cmx" + ) + + package "asciisyntax" ( + + description = "Coq asciisyntax plugin" + version = "8.7" + + requires = "" + directory = "syntax" + + archive(byte) = "ascii_syntax_plugin.cmo" + archive(native) = "ascii_syntax_plugin.cmx" + ) + + package "stringsyntax" ( + + description = "Coq stringsyntax plugin" + version = "8.7" + + requires = "coq.plugins.asciisyntax" + directory = "syntax" + + archive(byte) = "string_syntax_plugin.cmo" + archive(native) = "string_syntax_plugin.cmx" + ) + + package "derive" ( + + description = "Coq derive plugin" + version = "8.7" + + requires = "" + directory = "derive" + + archive(byte) = "derive_plugin.cmo" + archive(native) = "derive_plugin.cmx" + ) + + package "ssrmatching" ( + + description = "Coq ssrmatching plugin" + version = "8.7" + + requires = "coq.ltac" + directory = "ssrmatching" + + archive(byte) = "ssrmatching_plugin.cmo" + archive(native) = "ssrmatching_plugin.cmx" + ) + + package "ssreflect" ( + + description = "Coq ssreflect plugin" + version = "8.7" + + requires = "coq.plugins.ssrmatching" + directory = "ssr" + + archive(byte) = "ssreflect_plugin.cmo" + archive(native) = "ssreflect_plugin.cmx" + ) +) -- cgit v1.2.3 From d2c8d5cfcca2f4035782a385b6d94a01fa0394eb Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Tue, 16 Jan 2018 17:22:36 +0100 Subject: Rename coq.ltac to coq.plugins.ltac in META.coq --- META.coq | 51 +++++++++++++++++++++++++-------------------------- 1 file changed, 25 insertions(+), 26 deletions(-) diff --git a/META.coq b/META.coq index 9d0e948e6..d180820e8 100644 --- a/META.coq +++ b/META.coq @@ -240,19 +240,6 @@ package "stm" ( ) -package "ltac" ( - - description = "Coq LTAC Plugin" - version = "8.7" - - requires = "coq.stm" - directory = "plugins/ltac" - - archive(byte) = "ltac_plugin.cmo" - archive(native) = "ltac_plugin.cmx" - -) - package "toplevel" ( description = "Coq Toplevel" @@ -299,15 +286,27 @@ package "plugins" ( description = "Coq built-in plugins" version = "8.7" - requires = "" directory = "plugins" + package "ltac" ( + + description = "Coq LTAC Plugin" + version = "8.7" + + requires = "coq.stm" + directory = "ltac" + + archive(byte) = "ltac_plugin.cmo" + archive(native) = "ltac_plugin.cmx" + + ) + package "tauto" ( description = "Coq tauto plugin" version = "8.7" - requires = "coq.ltac" + requires = "coq.plugins.ltac" directory = "ltac" archive(byte) = "tauto_plugin.cmo" @@ -319,7 +318,7 @@ package "plugins" ( description = "Coq omega plugin" version = "8.7" - requires = "coq.ltac" + requires = "coq.plugins.ltac" directory = "omega" archive(byte) = "omega_plugin.cmo" @@ -343,7 +342,7 @@ package "plugins" ( description = "Coq micromega plugin" version = "8.7" - requires = "num,coq.ltac" + requires = "num,coq.plugins.ltac" directory = "micromega" archive(byte) = "micromega_plugin.cmo" @@ -355,7 +354,7 @@ package "plugins" ( description = "Coq quote plugin" version = "8.7" - requires = "coq.ltac" + requires = "coq.plugins.ltac" directory = "quote" archive(byte) = "quote_plugin.cmo" @@ -379,7 +378,7 @@ package "plugins" ( description = "Coq fourier plugin" version = "8.7" - requires = "coq.ltac" + requires = "coq.plugins.ltac" directory = "fourier" archive(byte) = "fourier_plugin.cmo" @@ -391,7 +390,7 @@ package "plugins" ( description = "Coq extraction plugin" version = "8.7" - requires = "coq.ltac" + requires = "coq.plugins.ltac" directory = "extraction" archive(byte) = "extraction_plugin.cmo" @@ -403,7 +402,7 @@ package "plugins" ( description = "Coq cc plugin" version = "8.7" - requires = "coq.ltac" + requires = "coq.plugins.ltac" directory = "cc" archive(byte) = "cc_plugin.cmo" @@ -415,7 +414,7 @@ package "plugins" ( description = "Coq ground plugin" version = "8.7" - requires = "coq.ltac" + requires = "coq.plugins.ltac" directory = "firstorder" archive(byte) = "ground_plugin.cmo" @@ -427,7 +426,7 @@ package "plugins" ( description = "Coq rtauto plugin" version = "8.7" - requires = "coq.ltac" + requires = "coq.plugins.ltac" directory = "rtauto" archive(byte) = "rtauto_plugin.cmo" @@ -439,7 +438,7 @@ package "plugins" ( description = "Coq btauto plugin" version = "8.7" - requires = "coq.ltac" + requires = "coq.plugins.ltac" directory = "btauto" archive(byte) = "btauto_plugin.cmo" @@ -463,7 +462,7 @@ package "plugins" ( description = "Coq nsatz plugin" version = "8.7" - requires = "num,coq.ltac" + requires = "num,coq.plugins.ltac" directory = "nsatz" archive(byte) = "nsatz_plugin.cmo" @@ -559,7 +558,7 @@ package "plugins" ( description = "Coq ssrmatching plugin" version = "8.7" - requires = "coq.ltac" + requires = "coq.plugins.ltac" directory = "ssrmatching" archive(byte) = "ssrmatching_plugin.cmo" -- cgit v1.2.3