aboutsummaryrefslogtreecommitdiff
path: root/META.coq
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-05-24 01:05:09 +0200
committerPierre-Marie Pédrot2018-05-24 01:05:09 +0200
commit9df6df865fc71ed9840fc569d3aa3cc7cf4750aa (patch)
tree8965b5d9bc37bc7d0be341dc311fef6df43c3616 /META.coq
parentb74d9500e5943317f1baf4f36b3d979d40f6105f (diff)
parentb4b515c2e61bc6ea662b48e84eb319ec8252b07d (diff)
Merge PR #6515: [api] Move `Vernacexpr` to parsing.
Diffstat (limited to 'META.coq')
-rw-r--r--META.coq4
1 files changed, 2 insertions, 2 deletions
diff --git a/META.coq b/META.coq
index 3414ccbd40..12d7666cb0 100644
--- a/META.coq
+++ b/META.coq
@@ -131,10 +131,10 @@ package "interp" (
package "grammar" (
- description = "Coq Base Grammar"
+ description = "Coq Camlp5 Grammar Extensions for Plugins"
version = "8.8"
- requires = "coq.interp"
+ requires = "camlp5.gramlib"
directory = "grammar"
archive(byte) = "grammar.cma"