diff options
| -rw-r--r-- | toplevel/class.ml | 17 | ||||
| -rw-r--r-- | toplevel/class.mli | 2 |
2 files changed, 8 insertions, 11 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index 75f4ee52d..463cfef5b 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -419,28 +419,25 @@ let process_coercion sec_sp (((coe,coeinfo),s,t) as x) = let t1 = process_cl sec_sp t in let p = (snd (class_info s1)).cL_PARAM in match coe with - | NAM_Var id -> ((coe,coeinfo),s1,t1),id,p + | NAM_Var id -> ((coe,coeinfo),s1,t1) | NAM_Constant sp -> if defined_in_sec sp sec_sp then let ((_,spid,spk)) = repr_path sp in let newsp = Lib.make_path spid CCI in - ((NAM_Constant newsp,coeinfo),s1,t1),spid,p + ((NAM_Constant newsp,coeinfo),s1,t1) else - ((coe,coeinfo),s1,t1),basename sp,p + ((coe,coeinfo),s1,t1) | NAM_Inductive (sp,i) -> if defined_in_sec sp sec_sp then let ((_,spid,spk)) = repr_path sp in let newsp = Lib.make_path spid CCI in - ((NAM_Inductive (newsp,i),coeinfo),s1,t1),spid,p + ((NAM_Inductive (newsp,i),coeinfo),s1,t1) else - ((coe,coeinfo),s1,t1),basename sp,p + ((coe,coeinfo),s1,t1) | NAM_Constructor ((sp,i),j) -> if defined_in_sec sp sec_sp then let ((_,spid,spk)) = repr_path sp in let newsp = Lib.make_path spid CCI in - let id = Global.id_of_global (ConstructRef ((newsp,i),j)) in - (((NAM_Constructor ((newsp,i),j)),coeinfo),s1,t1),id,p + (((NAM_Constructor ((newsp,i),j)),coeinfo),s1,t1) else - ((coe,coeinfo),s1,t1), - Global.id_of_global (ConstructRef ((sp,i),j)), - p + ((coe,coeinfo),s1,t1) diff --git a/toplevel/class.mli b/toplevel/class.mli index e88b3ccf0..57d395c20 100644 --- a/toplevel/class.mli +++ b/toplevel/class.mli @@ -21,4 +21,4 @@ val process_class : dir_path -> (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ) val process_coercion : dir_path -> (coe_typ * coe_info_typ) * cl_typ * cl_typ -> - ((coe_typ * coe_info_typ) * cl_typ * cl_typ) * identifier * int + (coe_typ * coe_info_typ) * cl_typ * cl_typ |