Two Applications of Logic Programming to Coq