diff options
| author | Pierre-Marie Pédrot | 2019-10-11 15:38:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-11 15:38:44 +0200 |
| commit | da116bcf6ed437743775ef09ff2e44217400f48c (patch) | |
| tree | 70955989d55fc3ab9e702029b81d79f58207b238 | |
| parent | c5f6186dd42f9eb937154953efeb2378d0bfb0ec (diff) | |
| parent | 82fd0993f2c677a080a58f7bc40d53a0b398c1cf (diff) | |
Merge PR #10804: Fix Print All of section variables
Reviewed-by: ppedrot
| -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 b6a0d9f39a..b24a97e2d4 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) |