The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

The recommended approach to update a development written for a version
prior to 8.0 is to use the Coq version 8.0 built-in translator. Indeed,
syntax has changed significantly and many lemmas have been renamed in
the move from generations 6 and 7 to generation 8. For instance, in
your case, the translator would automatically translate "congr_eqT"
into "f_equal".

Binary packages of Coq 8.0 are available at
ftp://ftp.inria.fr/INRIA/Projects/LogiCal/coq/V8.0pl4/ but I don't
know how compatible they are with recent versions of the common
platforms. If this does not work, the last bugfix version of Coq 8.0
should compile with recent versions of ocaml and camlp5 (get it with
"svn checkout svn://scm.gforge.inria.fr/svn/coq/branches/V8-0-bugfix").

To be automatically translated, the development has first to be
adapted to Coq 8.0 in old syntax mode (i.e. "coqtop -v7"). Then, it
can be translated using "coqtop -translate", or, for a whole directory
of files, by "tools/translate-v8". For a development made with some
version 6.X (which is the case for a 1998 development), the script
tools/translate_V6-3-1_to_V7-0 can be first used to upgrade to Coq 8.0
in old "v7" syntax mode. Some changes can still have to be made
afterwards to upgrade from 8.0 to 8.4, as typically indicated in files
CHANGES and COMPATIBILITY of the successive distributions.

If your development is small and you'd prefer to upgrade by hand,
searching for names of lemmas in theories7/*/*.v of the 8.0 archive
can also help. Look for the "only parsing" "Notation"s to know the new
name of old lemmas.

Hugo Herbelin

On Thu, Sep 13, 2012 at 08:37:47AM +0200, Nuno Gaspar wrote:
> Hello.
> 
> I'm restoring a development from 1998 to work with Coq 8.4 and I'm stuck 
> with
> some redefined/renamed lemma.
> 
> In short, where is the lemma congr_eqT that used to work with Coq v5.8?
> 
>   Lemma congr_eqT : (x==y)->((f x)==(f y)) 
>  
> I tried with SearchPattern, but no luck ...
> 
> Help please :-)
> 
> On a related note, regarding this particular development, there are a lot of
> proofs that were discharged by 'Auto' but now I find myself needing to use
> 'firstorder'. It is safe to conclude that that Auto/auto became
> less powerful through the years?
> 
> Cheers!
> 
> 
> --
> Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 
> dollars
> last year.
> Marge: Bart! Don't make fun of grad students, they just made a terrible life
> choice.