From 99129d2518bd9fe92051aa89138cbb57c839a270 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 28 Feb 2018 09:43:06 +0100
Subject: [ssreflect] Fix module scoping problems due to packing and mli files.

Unfortunately, mli-only files cannot be included in packs, so we have
the weird situation that the scope for `Tacexpr` is wrong. So we
cannot address the module as `Ltac_plugin.Tacexpr` but it lives in the
global namespace instead.

This creates problem when using other modular build/packing strategies
[such as #6857] This could be indeed considered a bug in the OCaml
compiler.

In order to remedy this situation we face two choices:
- leave the module out of the pack (!)
- create an implementation for the module

I chose the second solution as it seems to me like the most sensible
choice.

cc: #6512.
---
 dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh | 12 ++++++++++++
 dev/top_printers.mli                                        |  2 +-
 2 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh

(limited to 'dev')

diff --git a/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh b/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh
new file mode 100644
index 0000000000..5dedca0ca5
--- /dev/null
+++ b/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "6869" ] || [ "$CI_BRANCH" = "ssr+correct_packing" ]; then
+
+    Equations_CI_BRANCH=ssr+correct_packing
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    ltac2_CI_BRANCH=ssr+correct_packing
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+    Elpi_CI_BRANCH=ssr+correct_packing
+    Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
+
+fi
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index e47be638aa..dad6dcc1c0 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -153,7 +153,7 @@ val ppnamedcontextval : Environ.named_context_val -> unit
 val ppenv : Environ.env -> unit
 val ppenvwithcst : Environ.env -> unit
 
-val pptac : Tacexpr.glob_tactic_expr -> unit
+val pptac : Ltac_plugin.Tacexpr.glob_tactic_expr -> unit
 
 val ppobj : Libobject.obj -> unit
 
-- 
cgit v1.2.3