diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-03 18:13:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-03 18:23:54 +0200 |
| commit | 7525890df67fe711e2d3d63846ddb1e988d0812b (patch) | |
| tree | accc5678b182a6a65eb4ebd291f93da7f5779c27 /library | |
| parent | 4afe5e4385fc303010a4afd6040565ccd54291a9 (diff) | |
Fixing bug #2818.
Local Ltac definitions do not register their name in the nametab anymore,
thus elegantly solving the bug. The tactic body remains accessible from
the tactic engine, but the name is rendered meaningless to the userside.
Diffstat (limited to 'library')
| -rw-r--r-- | library/nametab.ml | 2 | ||||
| -rw-r--r-- | library/nametab.mli | 1 |
2 files changed, 3 insertions, 0 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index 3bd4e03ab..390789852 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -470,6 +470,8 @@ let exists_module = exists_dir let exists_modtype sp = MPTab.exists sp !the_modtypetab +let exists_tactic kn = KnTab.exists kn !the_tactictab + (* Reverse locate functions ***********************************************) let path_of_global ref = diff --git a/library/nametab.mli b/library/nametab.mli index eb2cecc59..e508c8617 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -127,6 +127,7 @@ val exists_modtype : full_path -> bool val exists_dir : DirPath.t -> bool val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) +val exists_tactic : full_path -> bool (** deprecated synonym of [exists_dir] *) (** {6 These functions locate qualids into full user names } *) |