From 1cc661d18f67f71a494b525b1f82fd9133ee5a3c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 3 Jul 2019 10:40:38 +0200
Subject: Move variable_secpath logic to dumpglob from constrintern

---
 interp/dumpglob.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'interp/dumpglob.ml')

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 482303d935..dc6a1ae180 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -166,6 +166,9 @@ let dump_reference ?loc modpath ident ty =
   let filepath = Names.DirPath.to_string (Lib.library_dp ()) in
   dump_ref ?loc filepath modpath ident ty
 
+let dump_secvar ?loc id =
+  dump_reference ?loc "<>" (Libnames.string_of_qualid (Decls.variable_secpath id)) "var"
+
 let dump_modref ?loc mp ty =
   let (dp, l) = Lib.split_modpath mp in
   let filepath = Names.DirPath.to_string dp in
-- 
cgit v1.2.3