- 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

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 :