From efc43d10527308cfc3ec358f9a14420add3735d0 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 19 Nov 2001 08:42:37 +0000
Subject: Renommage qualid_of_global en shortest_qualid_of_global

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2201 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/centaur.ml     | 6 +++---
 contrib/interface/name_to_ast.ml | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml
index bba7396b0d..eae99993f6 100644
--- a/contrib/interface/centaur.ml
+++ b/contrib/interface/centaur.ml
@@ -246,7 +246,7 @@ let add_search (global_reference:global_reference) assumptions cstr =
   try 
     let env = Global.env() in
     let id_string =
-      string_of_qualid (Nametab.qualid_of_global env global_reference) in
+      string_of_qualid (Nametab.shortest_qualid_of_global env global_reference) in
     let ast = 
     try
       CT_premise (CT_ident id_string, translate_constr assumptions cstr)
@@ -308,11 +308,11 @@ let globcv = function
   | Node(_,"MUTIND", (Path(_,sp))::(Num(_,tyi))::_) ->
       let env = Global.env() in
       convert_qualid
-	 (Nametab.qualid_of_global env (IndRef(sp,tyi)))
+	 (Nametab.shortest_qualid_of_global env (IndRef(sp,tyi)))
   | Node(_,"MUTCONSTRUCT",(Path(_,sp))::(Num(_,tyi))::(Num(_,i))::_) ->
       let env = Global.env() in
       convert_qualid
-          (Nametab.qualid_of_global env (ConstructRef ((sp, tyi), i)))
+          (Nametab.shortest_qualid_of_global env (ConstructRef ((sp, tyi), i)))
   | _ -> failwith "globcv : unexpected value";;
 
 let pbp_tac_pcoq =
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 8d3fd79c06..e961063689 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -110,7 +110,7 @@ let convert_one_inductive sp tyi =
   let env = Global.env () in
   let envpar = push_rel_context params env in
   ope("VERNACARGLIST",
-      [convert_qualid (Nametab.qualid_of_global env (IndRef (sp, tyi)));
+      [convert_qualid (Nametab.shortest_qualid_of_global env (IndRef (sp, tyi)));
        ope("CONSTR", [ast_of_constr true envpar arity]);
        ope("BINDERLIST", convert_env(List.rev params));
        convert_constructors envpar cstrnames cstrtypes]);;
-- 
cgit v1.2.3