From 653de32139ecee3114779a5ee2961c58793889e5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 6 Oct 2016 16:59:27 +0200
Subject: Ltac as a plugin.

This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
---
 dev/ocamldebug-coq.run | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 46caca8d6f..23ad1fc017 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -32,6 +32,6 @@ exec $OCAMLDEBUG \
         -I $COQTOP/plugins/ring       -I $COQTOP/plugins/romega \
 	-I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
         -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
-        -I $COQTOP/plugins/xml \
+        -I $COQTOP/plugins/xml        -I $COQTOP/plugins/ltac \
         -I $COQTOP/ide \
 	"$@"
-- 
cgit v1.2.3


From 6d49de4f2d1ed25b9a745378531a3b55bb0d8197 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 6 Oct 2016 18:39:28 +0200
Subject: Documenting the pluginification of Ltac.

---
 dev/doc/changes.txt | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index f54f3fcc8e..8d2d055908 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -40,6 +40,24 @@ important things:
 - Some printing functions were moved from Pptactic to Pputils
 - A part of Tacexpr has been moved to Tactypes
 
+The folder itself has been turned into a plugin. This does not change much,
+but because it is a packed plugin, it may wreak havoc for third-party plugins
+depending on any module defined in the ltac/ directory. Namely, even if
+everything looks OK at compile time, a plugin can fail to load at link time
+because it mistakenly looks for a module Foo instead of Ltac_plugin.Foo, with
+an error of the form:
+
+Error: while loading myplugin.cmxs, no implementation available for Foo.
+
+In particular, most EXTEND macros will trigger this problem even if they
+seemingly do not use any Ltac module, as their expansion do.
+
+The solution is simple, and consists in adding a statement "open Ltac_plugin"
+in each file using a Ltac module, before such a module is actually called. An
+alternative solution would be to fully qualify Ltac modules, e.g. turning any
+call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not
+work for EXTEND macros though.
+
 ** Error handling **
 
 - All error functions now take an optional parameter `?loc:Loc.t`. For
-- 
cgit v1.2.3