Déplacement de qualid dans Nametab, hors du noyau

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

5 files changed, 5 insertions, 11 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index ca8553525..630a8bb31 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -232,9 +232,9 @@ let strength_of_cl = function
 let string_of_class = function
   | CL_FUN -> "FUNCLASS"
   | CL_SORT -> "SORTCLASS" 
-  | CL_CONST sp -> string_of_qualid (Global.qualid_of_global (ConstRef sp))
-  | CL_IND sp -> string_of_qualid (Global.qualid_of_global (IndRef sp))
-  | CL_SECVAR sp -> string_of_qualid (Global.qualid_of_global (VarRef sp))
+  | CL_CONST sp -> Global.string_of_global (ConstRef sp)
+  | CL_IND sp -> Global.string_of_global (IndRef sp)
+  | CL_SECVAR sp -> Global.string_of_global (VarRef sp)
 
 (* coercion_value : int -> unsafe_judgment * bool *)
 
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index dbc717fc0..ff57b0012 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -13,9 +13,6 @@ let raise_pretype_error (loc,k,ctx,te) =
 let error_var_not_found_loc loc k s =
   raise_pretype_error (loc,k, Global.env() (*bidon*), VarNotFound s)
 
-let error_global_not_found_loc loc q =
-  raise_pretype_error (loc,CCI, Global.env() (*bidon*), QualidNotFound q)
-
 let error_cant_find_case_type_loc loc env expr =
   raise_pretype_error (loc, CCI, env, CantFindCaseType expr)
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 88f5889eb..a48329bd1 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -16,9 +16,6 @@ open Rawterm
 val error_var_not_found_loc :
   loc -> path_kind -> identifier -> 'a
 
-val error_global_not_found_loc :
-  loc -> qualid -> 'a
-
 val error_cant_find_case_type_loc : 
   loc -> env -> constr -> 'a
 
diff --git a/pretyping/syntax_def.mli b/pretyping/syntax_def.mli
index 84ef5e1d9..cbe1ba7e5 100644
--- a/pretyping/syntax_def.mli
+++ b/pretyping/syntax_def.mli
@@ -12,6 +12,6 @@ val declare_syntactic_definition : identifier -> rawconstr -> unit
 
 val search_syntactic_definition : section_path -> rawconstr
 
-val locate_syntactic_definition : qualid -> section_path
+val locate_syntactic_definition : Nametab.qualid -> section_path
 
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 1b4b89f8b..d942a6611 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -593,7 +593,7 @@ let unfold env sigma name =
 
 let string_of_evaluable_ref = function
   | EvalVarRef id -> string_of_id id
-  | EvalConstRef sp -> string_of_qualid (qualid_of_sp sp)
+  | EvalConstRef sp -> string_of_path sp
 
 (* [unfoldoccs : (readable_constraints -> (int list * section_path) -> constr -> constr)]
  * Unfolds the constant name in a term c following a list of occurrences occl.