diff options
author | Cyprien Mangin <cyprien.mangin@m4x.org> | 2018-01-16 17:22:36 +0100 |
---|---|---|
committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2018-01-16 17:22:36 +0100 |
commit | d2c8d5cfcca2f4035782a385b6d94a01fa0394eb (patch) | |
tree | 91ee2c94536f18d41a8f1dabfa7448146c76739e | |
parent | 638b820bf3e150ff295337189c505df351ca7e32 (diff) |
Rename coq.ltac to coq.plugins.ltac in META.coq
-rw-r--r-- | META.coq | 51 |
1 files changed, 25 insertions, 26 deletions
@@ -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" |