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).

1 files changed, 38 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/2729.v b/test-suite/bugs/closed/2729.v
index 3efca5d993..c0a4adcb3d 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.