From 4aa99307874c59f97570f624a06463aaa8115ec5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 6 Nov 2018 14:25:33 +0100
Subject: [vernac] Rename Vernacinterp to Vernacextend and move extension
 functions there.

This PR fixes an issues that was bugging me for some time, namely that
`Vernacinterp` really means `Vernacextend`.

We thus rename the file and move the associated functions there, which
were incorrectly placed in `Vernacentries`.

Note the beneficial effects on reducing the `.mli` API.
---
 grammar/dune | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'grammar/dune')

diff --git a/grammar/dune b/grammar/dune
index f03fe07607..78df2826d6 100644
--- a/grammar/dune
+++ b/grammar/dune
@@ -1,8 +1,7 @@
 (library
- (name grammar)
+ (name grammar5)
  (synopsis "Coq Camlp5 Grammar Extensions for Plugins")
  (public_name coq.grammar)
- (wrapped false)
  (flags (:standard -w -58))
  (libraries camlp5))
 
@@ -14,7 +13,7 @@
 
 (rule
  (targets coqp5)
- (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx %{dep:grammar.cmxa} -o coqp5)))
+ (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx %{dep:grammar5.cmxa} -o coqp5)))
 
 (install
  (section bin)
-- 
cgit v1.2.3