summaryrefslogtreecommitdiff
path: root/pretyping/termops.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-07-04 13:28:35 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2009-07-04 13:28:35 +0200
commite4282ea99c664d8d58067bee199cbbcf881b60d5 (patch)
treed4c4a873eb055c728666f367469fa26c3417793a /pretyping/termops.ml
parenta0a94c1340a63cdb824507b973393882666ba52a (diff)
Imported Upstream version 8.2.pl1+dfsgupstream/8.2.pl1+dfsg
Diffstat (limited to 'pretyping/termops.ml')
-rw-r--r--pretyping/termops.ml11
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