-let fix_lefts_in_constrs ~subst r_uri r_len context ty_term =
- assert false; (* BUG, ask enrico *)
- let _,_,itl,_,i = specialize_inductive_type_constrs ~subst context ty_term in
- let _,_,_,cl = List.nth itl i in
- let cl =
- List.map (fun (_,id,ty) -> id, debruijn r_uri r_len context ty) cl
+let specialize_and_abstract_constrs ~subst r_uri r_len context ty_term =
+ let cl = specialize_inductive_type_constrs ~subst context ty_term in
+ let len = List.length context in
+ let context_dcl =
+ match E.get_checked_obj r_uri with
+ | _,_,_,_, NCic.Inductive (_,_,tys,_) ->
+ context @ List.map (fun (_,name,arity,_) -> name,C.Decl arity) tys
+ | _ -> assert false