Author: Pierre Corbineau
Title: A reflexive tactic for first-order reasoning in Coq
Abstract: 
We propose a new implementation of a Coq tactic for
first-order reasoning, using reflection.  We produce a concrete
structure for proof traces that is checked by a Coq function, which we
proved correct. This method provides significant improvements
regarding efficiency, and size of the proof-terms produced.