From 870f7d0f833c288aa22a333df376e5cb8fbb403e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 24 Aug 2017 17:27:19 +0200
Subject: Program: fix BZ#5683, missing lift when building case predicate

---
 pretyping/cases.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3