Fixed incorrect optimization in Prettyp.pr_located_qualid introduced

in commit r12265. Add a few synonyms back in Libnames/Nameops to
maintain some minimal compatibility.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12267 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 25 insertions, 3 deletions

diff --git a/dev/base_include b/dev/base_include
index 711dcb2a1..b6c2e4d08 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -105,6 +105,8 @@ open Ppextend
 open Reserve
 open Syntax_def
 open Topconstr
+open Prettyp
+open Search
 
 open Clenvtac
 open Evar_refiner
@@ -180,7 +182,7 @@ let constr_of_string s =
 open Declarations;;
 
 let constbody_of_string s =
-  let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_sp (path_of_string s))) in
+  let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_string s)) in
   Option.get b.const_body;;
 
 (* Get the current goal *)
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 *)
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 538828fca..9e6ff72d3 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -205,7 +205,7 @@ let pr_located_qualid = function
 	| IndRef _ -> "Inductive"
 	| ConstructRef _ -> "Constructor"
 	| VarRef _ -> "Variable" in
-      str ref_str ++ spc () ++ pr_global ref
+      str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref)
   | Syntactic kn ->
       str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn)
   | Dir dir ->
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 024f190f2..1c7cfa9f6 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -362,7 +362,7 @@ let make_elim_fun (names,(nbfix,lv,n)) largs =
 
 let dummy = mkProp
 let vfx = id_of_string"_expanded_fix_"
-let vfun = id_of_string"_elimminator_function_"
+let vfun = id_of_string"_eliminator_function_"
 
 (* Mark every occurrence of substituted vars (associated to a function)
    as a problem variable: an evar that can be instantiated either by