I am porting some old proofs for 8.9 to 8.10.2 and immediately stumbled upon a problem. Consider this lemma:
Require Import CoLoR.Util.Vector.VecUtil. Import VectorNotations. Open Scope vector_scope. Lemma Vbuild_1 B gen: @Vbuild B 1 gen = [gen 0 (Arith.Lt.lt_0_Sn 0)]. Proof. unfold Vbuild. cbn. apply Vcons_eq. split. - apply f_equal, Peano_dec.le_unique. - reflexivity. Qed.
cbn step in Coq-8.9 the goal looks like:
[gen 0 (VecUtil.Vbuild_spec_obligation_4 gen eq_refl)] = [gen 0 (PeanoNat.Nat.lt_0_succ 0)]
However, with Coq 8.10.2 I get:
eq_rect 1 (fun H : nat => vector B H)
[gen 0 (VecUtil.Vbuild_spec_obligation_4 eq_refl)] 1
(VecUtil.Vbuild_spec_obligation_5 eq_refl) = [gen 0 (PeanoNat.Nat.lt_0_succ 0)]
Any ideas why? What is the recommended way of dealing with this? Thanks!