diff options
| author | Matthieu Sozeau | 2017-08-24 17:27:19 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2017-08-24 17:29:02 +0200 |
| commit | 870f7d0f833c288aa22a333df376e5cb8fbb403e (patch) | |
| tree | d1b661c38519196d685f1ad50e3529b7572a092b /pretyping | |
| parent | 7b1ff0c70a3ba9cd3cfa5aa6723f8f8a2b6e5396 (diff) | |
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 |