Fixing vm_compute bug #2729 (function used to decompose constructors

did not handle let-ins and was wrongly specified). Thanks to Pierre
Boutillier and Pierre-Marie Pédrot for pointing out the source of the
bug.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15027 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 81 insertions, 8 deletions

diff --git a/kernel/term.mli b/kernel/term.mli
index d5899f1855..a54130efa2 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -435,8 +435,7 @@ val it_mkProd_or_LetIn : types -> rel_context -> types
 (** {6 Other term destructors. } *)
 
 (** Transforms a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} into the pair
-   {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a product.
-   It includes also local definitions *)
+   {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a product. *)
 val decompose_prod : constr -> (name*constr) list * constr
 
 (** Transforms a lambda term {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index fad2e6f082..ac3df7149f 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -109,7 +109,7 @@ let build_branches_type env (mind,_ as _ind) mib mip params dep p =
      a 0) et les lambda correspondant aux realargs *)
   let build_one_branch i cty =
     let typi = type_constructor mind mib cty params in
-    let decl,indapp = Term.decompose_prod typi in
+    let decl,indapp = decompose_prod_assum typi in
     let ind,cargs = find_rectype_a env indapp in
     let nparams = Array.length params in
     let carity = snd (rtbl.(i)) in
@@ -193,11 +193,8 @@ and nf_stk env c t stk  =
       let bsw = branch_of_switch (nb_rel env) sw in
       let mkbranch i (n,v) =
 	let decl,codom = btypes.(i) in
-	let env =
-	  List.fold_right
-	    (fun (name,t) env -> push_rel (name,None,t) env) decl env in
-	let b = nf_val env v codom in
-	compose_lam decl b
+	let b = nf_val (push_rel_context decl env) v codom in
+	it_mkLambda_or_LetIn b decl
       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/shouldsucceed/2729.v b/test-suite/bugs/closed/shouldsucceed/2729.v
new file mode 100644
index 0000000000..44f8d3c7c9
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2729.v
@@ -0,0 +1,77 @@
+Require Import Equality.
+
+Parameter NameSet : Set.
+Parameter SignedName : Set.
+Parameter SignedName_compare : forall (x y : SignedName), comparison.
+Parameter pu_type : NameSet -> NameSet -> Type.
+Parameter pu_nameOf : forall {from to : NameSet}, pu_type from to -> SignedName.
+Parameter commute : forall {from mid1 mid2 to : NameSet},
+              pu_type from mid1 -> pu_type mid1 to
+           -> pu_type from mid2 -> pu_type mid2 to -> Prop.
+
+Program Definition castPatchFrom {from from' to : NameSet}
+                                 (HeqFrom : from = from')
+                                 (p : pu_type from to)
+                               : pu_type from' to
+    := p.
+
+Class PatchUniverse : Type := mkPatchUniverse {
+
+    commutable : forall {from mid1 to : NameSet},
+                        pu_type from mid1 -> pu_type mid1 to -> Prop
+        := fun {from mid1 to : NameSet}
+               (p : pu_type from mid1) (q : pu_type mid1 to) =>
+           exists mid2   : NameSet,
+           exists q' : pu_type from mid2,
+           exists p' : pu_type mid2 to,
+           commute p q q' p';
+
+    commutable_dec : forall {from mid to : NameSet}
+                            (p : pu_type from mid)
+                            (q : pu_type mid to),
+                     {mid2 : NameSet &
+                     { q' : pu_type from mid2 &
+                     { p' : pu_type mid2 to &
+                     commute p q q' p' }}}
+                   + {~(commutable p q)}
+}.
+
+Inductive SequenceBase (pu : PatchUniverse)
+                     : NameSet -> NameSet -> Type
+    := Nil : forall {cxt : NameSet},
+             SequenceBase pu cxt cxt
+     | Cons : forall {from mid to : NameSet}
+                     (p : pu_type from mid)
+                     (qs : SequenceBase pu mid to),
+              SequenceBase pu from to.
+Implicit Arguments Nil [pu cxt].
+Implicit Arguments Cons [pu from mid to].
+
+Program Fixpoint insertBase {pu : PatchUniverse}
+                            {from mid to : NameSet}
+                            (p : pu_type from mid)
+                            (qs : SequenceBase pu mid to)
+                          : SequenceBase pu from to
+    := match qs with
+       | Nil _ => Cons p Nil
+       | Cons mid' mid2' to' q qs' =>
+           match SignedName_compare (pu_nameOf p) (pu_nameOf q) with
+           | Lt => Cons p qs
+           | _  => match commutable_dec p (castPatchFrom _ q) with
+                   | inleft (existT _ (existT q' (existT p' _))) => Cons q'
+(insertBase p' qs')
+                   | inright _ => Cons p qs
+                   end
+           end
+       end.
+
+Lemma insertBaseConsLt {pu : PatchUniverse}
+                       {o op opq opqr : NameSet}
+                       (p : pu_type o op)
+                       (q : pu_type op opq)
+                       (rs : SequenceBase pu opq opqr)
+                       (p_Lt_q : SignedName_compare (pu_nameOf p) (pu_nameOf q)
+= Lt)
+                     : insertBase p (Cons q rs) = Cons p (Cons q rs).
+Proof.
+vm_compute.