let indtyno, (_,_,tys,_,_),leftno = match indty with
NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,leftno))) as r) ->
indtyno, NCicEnvironment.get_checked_indtys status r, leftno
| _ -> prerr_endline ("engine: indty expected... (fix this error message)"); assert false in
let (_,ind_name,_,_ as it) = List.nth tys indtyno in
let status,obj =
let indtyno, (_,_,tys,_,_),leftno = match indty with
NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,leftno))) as r) ->
indtyno, NCicEnvironment.get_checked_indtys status r, leftno
| _ -> prerr_endline ("engine: indty expected... (fix this error message)"); assert false in
let (_,ind_name,_,_ as it) = List.nth tys indtyno in
let status,obj =