The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Wed, Nov 19, 2014 at 10:26 AM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

Daniel,

I am not sure I understand your suggestion. Are we talking about
your definition of vector (for which you have 'vector_cons_proper')
or the one from standard library?

I am hesitant switching to new vector definition as it would entail
redoing a lot of my existing proofs.

I've replied privately to Vadim with my file, rewritten to use standard library Vector.t.  f_equiv works beautifully after changing Vector.cons to vcons_reord, though the rewrite still isn't working.

Snippet of the tactics I defined for this:

Ltac vcons_to_vcons_reord :=

match goal with |- context [Vector.cons ?A ?h ?n ?t] =>

  change (Vector.cons A h n t) with (@vcons_reord A n h t)

end.

Ltac vcons_equiv := repeat vcons_to_vcons_reord; f_equiv.

-- 

Daniel Schepler