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 | |
| 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
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index a92e374808..17fb5503cc 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1796,7 +1796,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred = (* First strategy: we build an "inversion" predicate *) let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in (* Second strategy: we directly use the evar as a non dependent pred *) - let pred2 = lift (List.length arsign) t in + let pred2 = lift (List.length (List.flatten arsign)) t in [sigma1, pred1; sigma, pred2] (* Some type annotation *) | Some rtntyp, _ -> |