In this note we compare two kinds of systems that verify the correctness of mathematical developments: proof checking and proof construction by tactics and we propose to merge them in a single system. We consider mathematics formalized in the Calculus of Constructions [3] [4] but the ideas given here are not specific to this formalism. As an example of a proof checking system we consider the constructive engine of the system Coq [11] and as an example of a proof construction by tactics system we consider the proof assistant of the system Coq [7] designed in the spirit of the system LCF [8]