Utilisation de global_reference dans rawconstr

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

1 files changed, 5 insertions, 5 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 306f2b8ce2..a452cf645e 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -137,11 +137,11 @@ let coercion_exists coe =
   with Not_found -> false
 
 let coe_of_reference = function
-  | RConst (sp,l) -> NAM_Constant sp
-  | RInd (ind_sp,l) -> NAM_Inductive ind_sp
-  | RConstruct (cstr_sp,l) -> NAM_Constructor cstr_sp
-  | RVar id  -> NAM_Var id
-  | _ -> raise Not_found
+  | ConstRef sp -> NAM_Constant sp
+  | IndRef sp -> NAM_Inductive sp
+  | ConstructRef sp -> NAM_Constructor sp
+  | VarRef sp  -> NAM_Var (basename sp)
+  | EvarRef _ -> raise Not_found
 
 let coercion_params r =
   let _,coe_info = coercion_info (coe_of_reference r) in