diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-26 22:27:32 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-26 22:27:32 +0000 |
| commit | ad306872932e37425158e1950a5b7465d28b22f0 (patch) | |
| tree | ccad8c9bc90ee62f56c03f438146f274a2f55437 /lib/util.mli | |
| parent | f22d5b55021fcf5fb11fa9d4fce3a7b8d9bc532f (diff) | |
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
Diffstat (limited to 'lib/util.mli')
| -rw-r--r-- | lib/util.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/util.mli b/lib/util.mli index 8f8475afd..380f58eab 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 |