The Coq mailing list

[Théo Zimmermann <theo AT irif.fr>]

Hi,

What you propose doesn't really sound like an efficient method to me. Worse, it would make your proofs very hard to maintain in the future, so what would you even gain from porting them to a new version?

What you *should* do is to refer to the release notes (https://coq.inria.fr/refman/changes.html), where all the breaking changes are documented and explained, often with strategies to port existing code. Then, you can learn why your proofs are broken:

Changed: The default tactic used by firstorder is auto with core instead of auto with *; [...] the default solver can be set with Set Firstorder Solver.

The easiest way to fix your main compatibility problem (although not the most robust) is therefore to set the default solver back to auto with *.

Best,

Théo

Le mar. 3 août 2021 à 10:48, mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> a écrit :

Hi Everyone,

2 years ago, I wrote a proof [1] using Coq 8.10 (if I remember
correctly), but now the proof can't get past Coq 8.12.2. With Coq
8.10, I used the 'firstorder' tactic generously, to build the terms,
and now most of these are broken.

My question is: how can I fix it with the least amount of effort?  One
idea that I have is to get the Coq 8.10 and replay the proof. From the
proof, get the Gallina terms by using 'Show Proof' and use the Gallina
terms directly to build the current proof.  I am curious if there is
another way to do this.


Best,
Mukesh

[1] https://github.com/mukeshtiwari/EncryptionSchulze/blob/master/code/Workingcode/ValidityExist.v#L83-L1460