From 82fd0993f2c677a080a58f7bc40d53a0b398c1cf Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 1 Oct 2019 15:48:09 +0200
Subject: Fix Print All of section variables

---
 tactics/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/declare.ml b/tactics/declare.ml
index e418240d3a..952ae023ad 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -347,7 +347,7 @@ let declare_variable ~name ~kind d =
   in
   Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
   Decls.(add_variable_data name {opaque;kind});
-  add_anonymous_leaf (inVariable ());
+  ignore(add_leaf name (inVariable ()) : Libobject.object_name);
   Impargs.declare_var_implicits ~impl name;
   Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name)
 
-- 
cgit v1.2.3