diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/termops.ml | 9 | ||||
| -rw-r--r-- | pretyping/termops.mli | 2 |
2 files changed, 11 insertions, 0 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 56e4f6ecce..a49f27ac5a 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -1074,6 +1074,15 @@ let assums_of_rel_context sign = | None -> (na, t)::l) sign ~init:[] +let fold_map_rel_context f env sign = + let rec aux env acc = function + | d::sign -> + aux (push_rel d env) (map_rel_declaration (f env) d :: acc) sign + | [] -> + acc + in + aux env [] (List.rev 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 diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 194fa71327..efa31b124d 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -267,6 +267,8 @@ val process_rel_context : (rel_declaration -> env -> env) -> env -> env val assums_of_rel_context : rel_context -> (name * constr) list val lift_rel_context : int -> rel_context -> rel_context val substl_rel_context : constr list -> rel_context -> rel_context +val fold_map_rel_context : + (env -> constr -> constr) -> env -> rel_context -> rel_context val map_rel_context_with_binders : (int -> constr -> constr) -> rel_context -> rel_context val fold_named_context_both_sides : |