4 files changed, 20 insertions, 0 deletions
diff --git a/library/libnames.ml b/library/libnames.ml
index 21be8f7d1..c7d484d1e 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -289,3 +289,8 @@ let pop_global_reference = function
   | IndRef (kn,i) -> IndRef (pop_kn kn,i)
   | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
   | VarRef id -> anomaly "VarRef not poppable"
+
+(* Deprecated synonyms *)
+
+let make_short_qualid = qualid_of_ident
+let qualid_of_sp = qualid_of_path
diff --git a/library/libnames.mli b/library/libnames.mli
index e6591734b..92dd9cb28 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -164,3 +164,8 @@ val loc_of_reference : reference -> loc
 val pop_con : constant -> constant
 val pop_kn : kernel_name -> kernel_name
 val pop_global_reference : global_reference -> global_reference
+
+(* Deprecated synonyms *)
+
+val make_short_qualid : identifier -> qualid (* = qualid_of_ident *)
+val qualid_of_sp : full_path -> qualid (* = qualid_of_path *)
diff --git a/library/nametab.ml b/library/nametab.ml
index a511a4e60..797f88e39 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -551,3 +551,8 @@ let _ =
       Summary.init_function = init;
       Summary.survive_module = false;
       Summary.survive_section = false }
+
+(* Deprecated synonyms *)
+
+let extended_locate = locate_extended
+let absolute_reference = global_of_path
diff --git a/library/nametab.mli b/library/nametab.mli
index 634e4d034..5367bfdd8 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -170,3 +170,8 @@ val shortest_qualid_of_syndef : Idset.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : module_path -> qualid
 val shortest_qualid_of_module : module_path -> qualid
 val shortest_qualid_of_tactic : ltac_constant -> qualid
+
+(* Deprecated synonyms *)
+
+val extended_locate : qualid -> extended_global_reference (*= locate_extended *)
+val absolute_reference : full_path -> global_reference (* = global_of_path *)