Ce travail s'articulera avec un projet plus large de refonte du langage de tactiques de Coq dont le but est notamment de rapprocher la bibliothèque standard de l'extension SSReflect.