diff options
| author | Maxime Dénès | 2017-08-31 12:41:35 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-31 12:41:35 +0200 |
| commit | bdfcbceb57cb8d04fea02da39dee6b8e7f75ad29 (patch) | |
| tree | e52f665cb7950456c2ee7a71e46525a377942099 /pretyping | |
| parent | b8ddc6e8b7788bfdb92ebd5238ca92c633b3e092 (diff) | |
| parent | 870f7d0f833c288aa22a333df376e5cb8fbb403e (diff) | |
Merge PR #995: Program: fix BZ#5683, missing lift when building case predicate
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 49f073d663..1a879f911b 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2501,14 +2501,14 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar in let tycon, arity = + let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in match tycon' with - | None -> let ev = mkExistential env evdref in ev, ev + | None -> let ev = mkExistential env evdref in ev, lift nar ev | Some t -> let pred = match prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t with | Some (evd, pred) -> evdref := evd; pred | None -> - let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in lift nar t in Option.get tycon, pred in |