Porting from Coq-8.10 vs 8.9

Using Coq
1

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.

After 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!

2

by the way here is the obligation:

VecUtil.Vbuild_spec_obligation_5
     : forall n p : nat, S p = n -> S p = n
3

The difference is probably due to CoLoR version mismatch: your Coq 8.9 result is in CoLoR 1.6.0, and Coq 8.10~ is in CoLoR 1.7.0.

The way obligations are handled for Vbuild has changed in between these versions: [compare].

4

Thanks! This is CoLoR-related indeed. I’ve opened a ticket there: https://github.com/fblanqui/color/issues/22