Fixing a (new) part of bug #2729.

By moving convert_concl to new proof engine, re-typecheckeing was
incidentally introduced. Re-typechecking revealed that vm bug #2729
was still open. Indeed, the vm was still producing an ill-typed term.

This commit fixes ill-typedness of the vm in #2729 when reconstructing
a "match" in an inductive type whose constructors have let-ins.

Another part is still open (see test-suite).

4 files changed, 55 insertions, 5 deletions

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index d6926dac3..5813cd416 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -222,6 +222,13 @@ let it_mkNamedProd_or_LetIn init = it_named_context_quantifier mkNamedProd_or_Le
 let it_mkNamedProd_wo_LetIn init = it_named_context_quantifier mkNamedProd_wo_LetIn ~init
 let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier mkNamedLambda_or_LetIn ~init
 
+let it_mkLambda_or_LetIn_from_no_LetIn c decls =
+  let rec aux k decls c = match decls with
+  | [] -> c
+  | (na,Some b,t)::decls -> mkLetIn (na,b,t,aux (k-1) decls (liftn 1 k c))
+  | (na,None,t)::decls -> mkLambda (na,t,aux (k-1) decls c)
+  in aux (List.length decls) (List.rev decls) c
+
 (* *)
 
 (* strips head casts and flattens head applications *)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index e01b3f455..1e3d2e4e9 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -58,6 +58,10 @@ val it_mkNamedProd_or_LetIn : types -> named_context -> types
 val it_mkNamedProd_wo_LetIn : types -> named_context -> types
 val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
 
+(* Ad hoc version reinserting letin, assuming the body is defined in
+   the context where the letins are expanded *)
+val it_mkLambda_or_LetIn_from_no_LetIn : constr -> rel_context -> constr
+
 val it_named_context_quantifier :
   (named_declaration -> 'a -> 'a) -> init:'a -> named_context -> 'a
 
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 758686aa9..37b86d1ba 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -116,7 +116,8 @@ let build_branches_type env (mind,_ as _ind) mib mip u params dep p =
      a 0) et les lambda correspondant aux realargs *)
   let build_one_branch i cty =
     let typi = type_constructor mind mib u cty params in
-    let decl,indapp = decompose_prod_assum typi in
+    let decl,indapp = Reductionops.splay_prod env Evd.empty typi in
+    let decl_with_letin,_ = decompose_prod_assum typi in
     let ((ind,u),cargs) = find_rectype_a env indapp in
     let nparams = Array.length params in
     let carity = snd (rtbl.(i)) in
@@ -130,7 +131,7 @@ let build_branches_type env (mind,_ as _ind) mib mip u params dep p =
 	mkApp(papp,[|dep_cstr|])
       else papp
     in
-    decl, codom
+    decl, decl_with_letin, codom
   in Array.mapi build_one_branch mip.mind_nf_lc
 
 let build_case_type dep p realargs c =
@@ -199,9 +200,9 @@ and nf_stk env c t stk  =
       (* calcul des branches *)
       let bsw = branch_of_switch (nb_rel env) sw in
       let mkbranch i (n,v) =
-	let decl,codom = btypes.(i) in
-	let b = nf_val (push_rel_context decl env) v codom in
-	it_mkLambda_or_LetIn b decl
+	let decl,decl_with_letin,codom = btypes.(i) in
+	let b = nf_val (Termops.push_rels_assum decl env) v codom in
+        Termops.it_mkLambda_or_LetIn_from_no_LetIn b decl_with_letin
       in
       let branchs = Array.mapi mkbranch bsw in
       let tcase = build_case_type dep p realargs c in
diff --git a/test-suite/bugs/closed/2729.v b/test-suite/bugs/closed/2729.v
index 3efca5d99..c0a4adcb3 100644
--- a/test-suite/bugs/closed/2729.v
+++ b/test-suite/bugs/closed/2729.v
@@ -1,3 +1,41 @@
+(* This bug report actually revealed two bugs in the reconstruction of
+   a term with "match" in the vm *)
+
+(* A simplified form of the first problem *)
+
+(* Reconstruction of terms normalized with vm when a constructor has *)
+(* let-ins arguments *)
+
+Record A : Type := C { a := 0 : nat; b : a=a }.
+Goal forall d:A, match d with C a b => b end = match d with C a b => b end.
+intro.
+vm_compute.
+(* Now check that it is well-typed *)
+match goal with |- ?c = _ => try (let x := type of c in idtac) || fail 2 end.
+Abort.
+
+(* A simplified form of the second problem *)
+
+Parameter P : nat -> Type.
+
+Inductive box A := Box : A -> box A.
+
+Axiom com : {m : nat & box (P m) }.
+
+Lemma L :
+  (let (w, s) as com' return (com' = com -> Prop) := com in
+   let (s0) as s0
+     return (existT (fun m : nat => box (P m)) w s0 = com -> Prop) := s in
+   fun _ : existT (fun m : nat => box (P m)) w (Box (P w) s0) = com =>
+   True) eq_refl.
+Proof.
+vm_compute.
+(* Now check that it is well-typed (the "P w" used to be turned into "P s") *)
+match goal with |- ?c => try (let x := type of c in idtac) || fail 2 end.
+Abort.
+
+(* Then the original report *)
+
 Require Import Equality.
 
 Parameter NameSet : Set.