The Coq mailing list

[Claude Marche <Claude.Marche AT lri.fr>]

There is

  http://coq.inria.fr/contribs/unification.html

which has been done by Joseph Rouyer from... Nancy !

You may also ask to Evelyne Contejean her contribution to AC-matching,
which is not available on the web as far as I know, but there is her
paper at RTA'04.

- Claude

>>>>> "Colin" == Colin Riba 
>>>>>Â <Colin.Riba AT loria.fr>
>>>>>  writes:

    Colin> Hi all
    Colin> I'm looking for a formalisation of first order unification in Coq.
    Colin> Can somebody tell me if there are contributions and/or papers on 
this topics ?

    Colin> Thanks
    Colin> Colin
    Colin> --------------------------------------------------------
    Colin> Bug reports: http://coq.inria.fr/bin/coq-bugs
    Colin> Archives: http://pauillac.inria.fr/pipermail/coq-club
    Colin>           http://pauillac.inria.fr/bin/wilma/coq-club
    Colin> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
| Claude Marché           | 
mailto:Claude.Marche AT lri.fr
 |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  ;|
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |