euh d'après ce que j'ai compris, la partie "allocation de registres" de CompCert serait encore en OCaml... mais qu'il serait possible d'intégrer les travaux de la thèse de Benoît Robillard (dont la soutenance a eu lieu cet après-midi ) pour avoir le tout entièrement en Coq (mais j'ai suivi un peu de loin )
Partager