diff options
Diffstat (limited to 'library/nametab.ml')
| -rw-r--r-- | library/nametab.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index 0172048af..3fa22aae3 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -470,6 +470,8 @@ let path_of_syndef kn = let dirpath_of_module mp = MPmap.find mp !the_modrevtab +let path_of_tactic kn = + KNmap.find kn !the_tacticrevtab (* Shortest qualid functions **********************************************) |