Nous présenterons une extension du mode Maple pour Coq (exposé de l'an passé), dont nous commencerons par faire des rappels. Il s'agissait d'importer, dans Coq, des calculs effectués par Maple sur les expressions algébriques dans les corps. Dès lors, il est possible soit de faire juste du calcul, qui ne requiert aucune validation, soit de faire du calcul dans une preuve, qui devra être prouvé correct dans Coq (approche sceptique). Dans le cas particulier des expressions algébriques sur un corps, les preuves de correction sont complètement automatiques et prises en charge par la tactique Field.
Nous verrons alors comment il est possible d'utiliser cette interface entre Maple et Coq non plus seulement pour faire du calcul mais aussi en vue d'accroître l'automatisation du système Coq. À titre d'exemple, nous décrirons le développement d'une procédure d'élimination des quantificateurs dans les corps algébriquement clos où l'interface a été étendue afin de traiter les calculs de pgcds (polynômiaux).