From ad306872932e37425158e1950a5b7465d28b22f0 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 26 Mar 2012 22:27:32 +0000
Subject: Unification: Added a heuristic to solve problems of the form
 ?x[t1..tm] = ?y[u1..un] when ?x occurs in u1..un with no (easy) way to know
 if it occurs in rigid position or not. Such equations typically come from
 matching problems such as "match a return ?T[a] with pair a1 a2 => a1 end"
 where, a is in type "?A * ?B", and, in the branch, the return clause, of the
 form "?T[pair ?A ?B a1 a2]", has to be unified with ?A.  This possible
 dependency is kept since commits r15060-15062. The heuristic is to restrict
 ?T so that the dependency is removed, leading to a behavior similar to the
 one existing before these commits.

This allows BGsection15.v, from contrib Ssreflect, to compile as it
did before these commits.

Also, removed one function exported without true need in r15061.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15092 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/util.ml  | 3 +++
 lib/util.mli | 1 +
 2 files changed, 4 insertions(+)

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index 2bbdc76cf9..a87b9f5107 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -457,6 +457,9 @@ let list_map4 f l1 l2 l3 l4 =
   in
   map (l1,l2,l3,l4)
 
+let list_map_to_array f l =
+  Array.of_list (List.map f l)
+
 let rec list_smartfilter f l = match l with
     [] -> l
   | h::tl ->
diff --git a/lib/util.mli b/lib/util.mli
index 8f8475afd7..380f58eaba 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -101,6 +101,7 @@ val list_map3 :
   ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
 val list_map4 :
   ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
+val list_map_to_array : ('a -> 'b) -> 'a list -> 'b array
 val list_filter_i :
   (int -> 'a -> bool) -> 'a list -> 'a list
 
-- 
cgit v1.2.3