diff options
| author | herbelin | 2012-12-17 17:53:04 +0000 |
|---|---|---|
| committer | herbelin | 2012-12-17 17:53:04 +0000 |
| commit | d09a4df287a125162601e5970bb19aa278be91d6 (patch) | |
| tree | 4753c826104846606edbf2946bb56f6d8c2e05fc /kernel/type_errors.ml | |
| parent | 29413af72253682b182b5932e906c82f022b04e2 (diff) | |
Fixed a bug in the algorithm trying to elaborate a "match" return predicate.
This occurred in a second choice strategy which is anyway probably not
used in general, but the bug showed up in error messages since these
messages reports on the second choice when the first choice has failed
because of user-side typing error.
Anyway, having two strategies for building a return predicate will
probably eventually disappear with the increase of the strength of
unification.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16078 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions