diff options
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 668b3a1eb4..d01c5679cc 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -989,14 +989,18 @@ let assums_of_rel_context sign = | None -> (na, t)::l) sign ~init:[] -let lift_rel_context n sign = - let rec liftrec k = function - | (na,c,t)::sign -> - (na,option_map (liftn n k) c,type_app (liftn n k) t) - ::(liftrec (k-1) sign) +let map_rel_context_with_binders f sign = + let rec aux k = function + | d::sign -> map_rel_declaration (f k) d :: aux (k-1) sign | [] -> [] in - liftrec (rel_context_length sign) sign + aux (rel_context_length sign) sign + +let substl_rel_context l = + map_rel_context_with_binders (fun k -> substnl l (k-1)) + +let lift_rel_context n = + map_rel_context_with_binders (liftn n) let fold_named_context_both_sides f l ~init = list_fold_right_and_left f l init |