id_of_global devient sp_of_global

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

1 files changed, 12 insertions, 8 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 3b2dff70d9..9efa5aa4a5 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -161,12 +161,15 @@ let get_applist = whd_stack
 exception Destruct
 
 let dest_const_apply t = 
-  let f,args = get_applist t in 
+  let f,args = get_applist t in
+  let ref = 
   match kind_of_term f with 
-    | IsConst (sp,_) -> 	Global.id_of_global (ConstRef sp),args
-    | IsMutConstruct (csp,_) -> Global.id_of_global (ConstructRef csp),args
-    | IsMutInd (isp,_)       -> Global.id_of_global (IndRef isp),args
-    | _ -> raise Destruct 
+    | IsConst (sp,_)         ->	ConstRef sp
+    | IsMutConstruct (csp,_) -> ConstructRef csp
+    | IsMutInd (isp,_)       -> IndRef isp
+    | _ -> raise Destruct
+  in
+  basename (Global.sp_of_global ref), args
 
 type result = 
   | Kvar of string
@@ -178,11 +181,12 @@ let destructurate t =
   let c, args = get_applist t in
   match kind_of_term c, args with
     | IsConst (sp,_), args ->
-	Kapp (string_of_id (Global.id_of_global (ConstRef sp)),args)
+	Kapp (string_of_id (basename (Global.sp_of_global (ConstRef sp))),args)
     | IsMutConstruct (csp,_) , args ->
-	Kapp (string_of_id (Global.id_of_global (ConstructRef csp)),args)
+	Kapp (string_of_id (basename (Global.sp_of_global (ConstructRef csp))),
+			    args)
     | IsMutInd (isp,_), args ->
-	Kapp (string_of_id (Global.id_of_global (IndRef isp)),args)
+	Kapp (string_of_id (basename (Global.sp_of_global (IndRef isp))),args)
     | IsVar id,[] -> Kvar(string_of_id id)
     | IsProd (Anonymous,typ,body), [] -> Kimp(typ,body)
     | IsProd (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal"