From b8de2bae178a63a6c482a46ee01e5183676984ee Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 28 Nov 2018 02:33:37 +0100
Subject: [ltac] Remove aliases already present in the lower layers.

We remove a few aliases present in the lower layers
[`Genintern/Tactypes`] from `Tacexpr`.

IMHO this enlarges the API for no good purpose, and difficults
analysis.
---
 plugins/ltac/tacinterp.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'plugins/ltac/tacinterp.mli')

diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index f9883e4441..d9c80bb835 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -43,6 +43,8 @@ type interp_sign = Geninterp.interp_sign = {
   lfun : value Id.Map.t;
   extra : TacStore.t }
 
+open Genintern
+
 val f_avoid_ids : Id.Set.t TacStore.field
 val f_debug : debug_info TacStore.field
 
-- 
cgit v1.2.3