Le projet coq-hol-light est une bibliothèque Coq contenant une traduction automatique de la bibliothèque HOL-Light, utilisant hol2dk et lambdapi. Cette bibliothèque fournit des axiomes pour les théorèmes traduits, permettant une vérification rapide dans Coq. Elle vise à fournir une bibliothèque directement utilisable dans Coq, alignant les fonctions et prédicats HOL-Light sur ceux définis dans la bibliothèque standard Coq.

Cette bibliothèque fournit des fichiers vernaculaires contenant une formalisation de l'analyse réelle pour l'assistant de preuve Coq. Elle est une extension conservative de la bibliothèque standard Reals avec un accent sur l'utilisabilité.