diff options
Diffstat (limited to 'library/libnames.mli')
| -rw-r--r-- | library/libnames.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/library/libnames.mli b/library/libnames.mli index b00d51dc5..ffb51ec0b 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -82,9 +82,6 @@ type extended_global_reference = | TrueGlobal of global_reference | SyntacticDef of kernel_name -val subst_ext : - substitution -> extended_global_reference -> extended_global_reference - (*s Temporary function to brutally form kernel names from section paths *) val encode_kn : dir_path -> identifier -> kernel_name |