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 +
 test-suite/bugs/closed/bug_10917.v | 4 ++++
 2 files changed, 5 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_10917.v

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
diff --git a/test-suite/bugs/closed/bug_10917.v b/test-suite/bugs/closed/bug_10917.v
new file mode 100644
index 0000000000..cdb132ede0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10917.v
@@ -0,0 +1,4 @@
+(* This was raising an anomaly *)
+
+Definition m (h : 0 = 1) P : P 1 -> P 0 :=
+  fun H => match h, H with end.
-- 
cgit v1.2.3