The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

Hi,

It may be of some help if you want to use your unification in 
some extracted code.
I've an exact correctness proof of the unification algorithm given by John 
Harrison

http://www.cl.cam.ac.uk/users/jrh/atp/index.html

It is exact in the sense that the extracted code is as close as possible
to John's implementation (unfortunately it can't be exactly the same 
since John is using exceptions). If you are interested the code is here

ftp://ftp-sop.inria.fr/lemme/Laurent.Thery/unif.tar.gz

--
Laurent