The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

This is probably 
https://coq.inria.fr/distrib/V8.12.2/refman/changes.html#tactics
>Changed: The default tactic used by firstorder is auto with core instead of 
auto with *; see Decision procedures for details; old behavior can be reset by 
using the -compat 8.12 command-line flag; to ease the migration of legacy code, 
the default solver can be set to debug auto with * with Set Firstorder Solver 
debug auto with * (#11760, by Vincent Laporte).

Gaëtan Gilbert

On 03/08/2021 10:47, mukesh tiwari wrote:
> 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