diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-12-29 10:57:43 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-12-29 10:57:43 +0100 |
| commit | bf12eb93f3f6a6a824a10878878fadd59745aae0 (patch) | |
| tree | 279f64f4b7e4804415ab5731cc7aaa8a4fcfe074 /pretyping/cases.ml | |
| parent | e0d682ec25282a348d35c5b169abafec48555690 (diff) | |
Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg
Diffstat (limited to 'pretyping/cases.ml')
| -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 1819dc52..38355cf1 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1763,7 +1763,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, _ -> |