From 92696abcaab68c70461c285ada87e50dacf3bb34 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 8 Apr 2009 12:58:07 +0000
Subject: - Backport of 12053 (fixing parsing segfault bug #2087) and 12058
 (fixing   Not_found bug in Theorem with) from V8.2 to trunk. - Improving
 indentation in presence of tabulation and utf-8 when   reporting error
 messages with "^^^^^^". - Updating a few svn:ignore properties.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12059 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/termops.ml  | 9 +++++++++
 pretyping/termops.mli | 2 ++
 2 files changed, 11 insertions(+)

(limited to 'pretyping')

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 :
-- 
cgit v1.2.3