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.
---
 plugins/funind/indfun.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind/indfun.mli')

diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 93e03852ec..dcc1c2ea6a 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -14,7 +14,7 @@ val functional_induction :
   bool ->
   EConstr.constr ->
   (EConstr.constr * EConstr.constr bindings) option ->
-  Tacexpr.or_and_intro_pattern option ->
+  Ltac_plugin.Tacexpr.or_and_intro_pattern option ->
   Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
 
-- 
cgit v1.2.3