MIXDRECS: code coq presque non commente.

Pour plus quelques explications, voir:
http://www-lsr.imag.fr/Les.Personnes/Sylvain.Boulme/focal.html

COMPILATION: il suffit de faire "make"
version de coq utilisee:
The Coq Proof Assistant, version 8.0pl1 (Jul 2004)
compiled on jui 19 2004 18:38:29
