i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
) (0,[]) tyl) in
let con_env = DisambiguateTypes.env_of_list name_to_uris env in
- let undebrujin t =
- snd
- (List.fold_right
- (fun (name,_,_,_) (i,t) ->
- (*here the explicit_named_substituion is assumed to be of length 0 *)
- let t' = Cic.MutInd (uri,i,[]) in
- let t = CicSubstitution.subst t' t in
- i - 1,t
- ) tyl (List.length tyl - 1,t)) in
let tyl =
List.map
(fun (name,b,ty,cl) ->
let ty' =
add_params (interpretate_term context con_env None false ty)
in
- name,undebrujin ty'
+ name,ty'
) cl
in
name,b,ty',cl'