From a5b552175253726a3cd73471a96b33215ee19af2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 20 Feb 2020 01:44:32 +0100
Subject: Fixes #10917 (missing lift in building return clause by inversion).

---
 pretyping/cases.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index abc16f621e..55c1f41c2c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1817,6 +1817,7 @@ let build_inversion_problem ~program_mode loc env sigma tms t =
         List.rev_append patl patl',acc_sign,acc
     | (t, NotInd (bo,typ)) :: tms ->
       let pat,acc = make_patvar t acc in
+      let typ = lift n typ in
       let d = LocalAssum (annotR (alias_of_pat pat),typ) in
       let patl,acc_sign,acc = aux (n+1) (snd (push_rel ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma d env)) (d::acc_sign) tms acc in
       pat::patl,acc_sign,acc in
-- 
cgit v1.2.3