diff options
author | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:35 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:35 +0200 |
commit | e4282ea99c664d8d58067bee199cbbcf881b60d5 (patch) | |
tree | d4c4a873eb055c728666f367469fa26c3417793a /pretyping/termops.ml | |
parent | a0a94c1340a63cdb824507b973393882666ba52a (diff) |
Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg
Diffstat (limited to 'pretyping/termops.ml')
-rw-r--r-- | pretyping/termops.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index f93212f8..4f38fbb3 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: termops.ml 11639 2008-11-27 17:48:32Z barras $ *) +(* $Id: termops.ml 12058 2009-04-08 10:54:59Z herbelin $ *) open Pp open Util @@ -1017,6 +1017,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 |