diff options
| author | herbelin | 2000-11-23 14:04:38 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-23 14:04:38 +0000 |
| commit | 2dc9c764ea5ebc79ce5af4c8603316cefa94ce71 (patch) | |
| tree | 70a2434024e950448c4551ca24366c0d8cd4ec51 | |
| parent | ce788b8db752a987510e1f35c5e6b45eb0666066 (diff) | |
Informations inutiles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@925 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 75f4ee52d9..463cfef5bf 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 e88b3ccf02..57d395c207 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 |