diff options
| author | Gaëtan Gilbert | 2019-10-01 15:48:09 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-01 15:48:25 +0200 |
| commit | 82fd0993f2c677a080a58f7bc40d53a0b398c1cf (patch) | |
| tree | 8bb84fc26453e34c28a526999f173a57ae374e7d /tactics | |
| parent | 77fd11a9f012a2878e13451e9d8a9f500c6392eb (diff) | |
Fix Print All of section variables
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) |