From 55e1a9e3b6979f70edf5e80f26d358604d267d26 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 15 Sep 2023 12:32:46 +0200
Subject: [PATCH] Fix relevance check in typing.ml

---
 pretyping/typing.ml           | 2 ++
 test-suite/bugs/bug_17836_2.v | 6 ++++++
 2 files changed, 8 insertions(+)
 create mode 100644 test-suite/bugs/bug_17836_2.v

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 57a394361ac51..51418efaa9c14 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -200,6 +200,8 @@ let judge_of_case env sigma case ci pj iv cj lfj =
   let () = if Inductive.is_private specif then Type_errors.error_case_on_private_ind env ind in
   let indspec = ((ind, EInstance.kind sigma u), spec) in
   let sigma, (bty,rslty,rci) = type_case_branches env sigma indspec specif pj cj.uj_val in
+  (* TODO evar map aware check_case_info and should_invert_case *)
+  let ci = { ci with ci_relevance = Evarutil.nf_relevance sigma ci.ci_relevance } in
   let () = check_case_info env (fst indspec) rci ci in
   let sigma = check_branch_types env sigma (fst indspec) cj (lfj,bty) in
   let () = if (match iv with | NoInvert -> false | CaseInvert _ -> true) != should_invert_case env ci
diff --git a/test-suite/bugs/bug_17836_2.v b/test-suite/bugs/bug_17836_2.v
new file mode 100644
index 0000000000000..6fa554d39ac0d
--- /dev/null
+++ b/test-suite/bugs/bug_17836_2.v
@@ -0,0 +1,6 @@
+
+Lemma foo (n:nat) : match n with 0 => 0 | _ => 1 end = 0.
+Proof.
+  set (m := match n with 0 => _ | _ => _ end).
+  Validate Proof.
+Abort.