Merge PR #6593: Add plugins to META.coq

1 files changed, 297 insertions, 13 deletions

diff --git a/META.coq b/META.coq
index f7998db8e..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"
@@ -293,3 +280,300 @@ package "ide" (
   archive(native)  = "ide.cmxa"
 
 )
+
+package "plugins" (
+
+  description = "Coq built-in plugins"
+  version     = "8.7"
+
+  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.plugins.ltac"
+    directory   = "ltac"
+
+    archive(byte)    = "tauto_plugin.cmo"
+    archive(native)  = "tauto_plugin.cmx"
+  )
+
+  package "omega" (
+
+    description = "Coq omega plugin"
+    version     = "8.7"
+
+    requires    = "coq.plugins.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.plugins.ltac"
+    directory   = "micromega"
+
+    archive(byte)    = "micromega_plugin.cmo"
+    archive(native)  = "micromega_plugin.cmx"
+  )
+
+  package "quote" (
+
+    description = "Coq quote plugin"
+    version     = "8.7"
+
+    requires    = "coq.plugins.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.plugins.ltac"
+    directory   = "fourier"
+
+    archive(byte)    = "fourier_plugin.cmo"
+    archive(native)  = "fourier_plugin.cmx"
+  )
+
+  package "extraction" (
+
+    description = "Coq extraction plugin"
+    version     = "8.7"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "extraction"
+
+    archive(byte)    = "extraction_plugin.cmo"
+    archive(native)  = "extraction_plugin.cmx"
+  )
+
+  package "cc" (
+
+    description = "Coq cc plugin"
+    version     = "8.7"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "cc"
+
+    archive(byte)    = "cc_plugin.cmo"
+    archive(native)  = "cc_plugin.cmx"
+  )
+
+  package "ground" (
+
+    description = "Coq ground plugin"
+    version     = "8.7"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "firstorder"
+
+    archive(byte)    = "ground_plugin.cmo"
+    archive(native)  = "ground_plugin.cmx"
+  )
+
+  package "rtauto" (
+
+    description = "Coq rtauto plugin"
+    version     = "8.7"
+
+    requires    = "coq.plugins.ltac"
+    directory   = "rtauto"
+
+    archive(byte)    = "rtauto_plugin.cmo"
+    archive(native)  = "rtauto_plugin.cmx"
+  )
+
+  package "btauto" (
+
+    description = "Coq btauto plugin"
+    version     = "8.7"
+
+    requires    = "coq.plugins.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.plugins.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.plugins.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"
+  )
+)