From 99129d2518bd9fe92051aa89138cbb57c839a270 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
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.
---
 plugins/ltac/pptactic.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac/pptactic.ml')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 5d262ffcb..11bb7a234 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -14,11 +14,9 @@ open Namegen
 open CErrors
 open Util
 open Constrexpr
-open Tacexpr
 open Genarg
 open Geninterp
 open Stdarg
-open Tacarg
 open Libnames
 open Notation_term
 open Misctypes
@@ -29,6 +27,9 @@ open Pputils
 open Ppconstr
 open Printer
 
+open Tacexpr
+open Tacarg
+
 module Tag =
 struct
 
-- 
cgit v1.2.3