Merge PR #18195: Fix cbv evar case

Reviewed-by: ppedrot
Reviewed-by: herbelin
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

doc/changelog/04-tactics/18195-rewrite-rules.rst

@@ -0,0 +1,5 @@
+- **Fixed:**
+  Apply substitution in Case stack node for cbv reify
+  (`#18195 <https://github.com/coq/coq/pull/18195>`_,
+  fixes `#18194 <https://github.com/coq/coq/issues/18194>`_,
+  by Yann Leray).

pretyping/cbv.ml

@@ -371,7 +371,7 @@ let rec reify_stack t = function
       reify_stack (mkApp(t,Array.map_of_list reify_value args)) st
   | CASE (u,pms,ty,br,iv,ci,env,st) ->
       reify_stack
-        (mkCase (ci, u, pms, ty, iv, t,br))
+        (apply_env env @@ mkCase (ci, u, pms, ty, iv, t,br))
         st
   | PROJ (p, st) ->
        reify_stack (mkProj (p, t)) st

test-suite/bugs/bug_18194.v

@@ -0,0 +1,19 @@
+Require Import Coq.Program.Tactics.
+
+Program Definition a := Eval cbv zeta in (fun (a : True) => (?[A] : nat),
+  let r :=
+    let b := I in match tt with tt => b end
+  in
+  ?A@{a := r},
+  fun (a : True) => (eq_refl : ?A = _)).
+
+Next Obligation.
+  destruct a; exact 0.
+Defined.
+(* This used to fail with the message:
+File "test-suite/bugs/bug_18194.v", line 12, characters 0-8:
+Error:
+Unbound reference: In environment
+anonymous' : unit
+The reference 3 is free.
+*)