From bf4112094feb1a705d8bdaea3fb0febc4ef3ff59 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 24 Oct 2017 14:35:25 +0200
Subject: [general] Remove Econstr dependency from `intf`

To this extent we factor out the relevant bits to a new file,
ltac_pretype.
---
 dev/top_printers.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ffa8fffdf5..70f7c4283f 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -108,8 +108,7 @@ let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l)
 let ppunbound_ltac_var_map l = ppidmap (fun _ arg ->
   str"<genarg:" ++ pr_argument_type(genarg_tag arg) ++ str">")
 
-open Glob_term
-
+open Ltac_pretype
 let rec pr_closure {idents=idents;typed=typed;untyped=untyped} =
   hov 1 (str"{idents=" ++ prididmap idents ++ str";" ++ spc() ++
          str"typed=" ++ prconstrunderbindersidmap typed ++ str";" ++ spc() ++
-- 
cgit v1.2.3