Fix relevance check in typing.ml

SkySkimmer · Sep 15, 2023 · 55e1a9e · 55e1a9e
1 parent f640eef
commit 55e1a9e
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git 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
@@ -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.