From 7525890df67fe711e2d3d63846ddb1e988d0812b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 3 Sep 2014 18:13:07 +0200 Subject: 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. --- library/nametab.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'library/nametab.mli') 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 } *) -- cgit v1.2.3