Merge PR #16229: Fix incorrect generated letin handling in Program Cases

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

pretyping/cases.ml

@@ -2638,7 +2638,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
           | Some (evd, pred, arsign) -> evd, pred
           | None -> sigma, lift nar t
         in
-        sigma, Option.get tycon, pred
+        sigma, lift (List.length tomatchs_lets) (Option.get tycon), pred
   in
   let neqs, arity =
     let ctx = context_of_arsign eqs in
@@ -2703,6 +2703,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
     (* We check for unused patterns *)
     check_unused_pattern !!env used matx;
     let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in
+    let tycon = it_mkProd_wo_LetIn tycon tomatchs_lets in
     let j =
       { uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
         (* XXX: is this normalization needed? *)

test-suite/bugs/bug_16043.v

@@ -0,0 +1,52 @@
+Require Program.Tactics.
+
+Module Reduced.
+  Axiom t : Type -> Type.
+  Axiom map2 : forall {elt : Type}, t elt.
+
+  Program Definition map2' elt : t elt
+    := let f' := match true with
+                 | true => @None elt
+                 | _ => None
+                 end
+       in
+       map2.
+(* Error: Unbound reference: In environment
+elt : Type
+The reference 2 is free.
+ *)
+  About map2'.
+End Reduced.
+
+Require Coq.FSets.FMapInterface.
+Import Coq.Structures.Orders.
+Import Coq.FSets.FMapInterface.
+
+Definition option_value {A} (v1 : option A) (v2 : A) : A := match v1 with Some v => v | None => v2 end.
+
+Module ProdWSfun_gen (E1 : DecidableTypeOrig) (E2 : DecidableTypeOrig) (M1 : WSfun E1) (M2 : WSfun E2).
+
+  Definition t elt := M1.t { m : M2.t elt | ~M2.Empty m }.
+  Program Definition map2 elt elt' elt'' (f : option elt -> option elt' -> option elt'') : t elt -> t elt' -> t elt''
+    := let f' := match f None None with
+                 | None => f
+                 | _ => fun x y => match x, y with
+                                   | None, None => None
+                                   | _, _ => f x y
+                                   end
+                 end in
+       M1.map2 (fun m1 m2
+                => if match m1, m2 with None, None => true | _, _ => false end
+                   then None
+                   else
+                     let m1' := option_value (option_map (@proj1_sig _ _) m1) (M2.empty _) in
+                     let m2' := option_value (option_map (@proj1_sig _ _) m2) (M2.empty _) in
+                     let m' := M2.map2 f' m1' m2' in
+                     if M2.is_empty m'
+                     then None
+                     else Some (exist _ m' _)).
+  (* uncaught Not_found *)
+  Next Obligation. Admitted.
+  About map2.
+
+End ProdWSfun_gen.