From aaa56145f319b58300ed7f914b35eb11321838e4 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 18 May 2000 08:14:28 +0000 Subject: Effets de bords suite à la restructuration des inductives (cf Inductive) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@442 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/detyping.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) (limited to 'pretyping/detyping.ml') diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 0f3a36153..091c14a2e 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -102,24 +102,23 @@ let ids_of_env = Sign.ids_of_env (* Tools for printing of Cases *) let encode_inductive id = - let (refsp,tyi as indsp) = + let (indsp,_ as ind) = try - let sp = Nametab.sp_of_id CCI id in - match global_operator sp id with - | MutInd ind_sp,_ -> ind_sp + match kind_of_term (global_reference CCI id) with + | IsMutInd (indsp,args) -> (indsp,args) | _ -> errorlabstrm "indsp_of_id" [< 'sTR ((string_of_id id)^" is not an inductive type") >] with Not_found -> error ("Cannot find reference "^(string_of_id id)) in - let mip = mind_nth_type_packet (Global.lookup_mind refsp) tyi in - let constr_lengths = Array.map List.length mip.mind_listrec in + let mis = Global.lookup_mind_specif ind in + let constr_lengths = Array.map List.length (mis_recarg mis) in (indsp,constr_lengths) let sp_of_spi (refsp,tyi) = - let mip = mind_nth_type_packet (Global.lookup_mind refsp) tyi in + let mip = Constant.mind_nth_type_packet (Global.lookup_mind refsp) tyi in let (pa,_,k) = repr_path refsp in - make_path pa mip.mind_typename k + make_path pa mip.Constant.mind_typename k (* let (_,mip) = mind_specif_of_mind_light spi in -- cgit v1.2.3