- (fun i -> NCic.Const (NReference.reference_of_spec uri
- (NReference.Ind (ind,i,leftno))))
- (List.rev (HExtlib.list_seq 0 (List.length itl)))
- te
- in
- metasenv,subst,(k_relev,n,te)::res
+ (fun i ->
+ if i <= leftno then
+ NCic.Rel i
+ else
+ NCic.Const (NReference.reference_of_spec uri
+ (NReference.Ind (ind,relsno - i,leftno))))
+ (HExtlib.list_seq 1 (relsno+1))
+ te in
+ let te =
+ List.fold_right
+ (fun (name,decl) te ->
+ match decl with
+ NCic.Decl ty -> NCic.Prod (name,ty,te)
+ | NCic.Def (bo,ty) -> NCic.LetIn (name,ty,bo,te)
+ ) sx_context_te_rev te
+ in
+ metasenv,subst,(k_relev,n,te)::res