It is commonly agreed that the success of future proof assistants will rely in their ability to incorporate computations within deductions in order to mimic the mathematician when replacing the proof of a proposition P by the proof of an equivalent proposition P' obtained from $P$ thanks to possibly complex calculations. In this paper, we investigate a new version of the calculus of constructions in which computations are based on Shostak's congruence closure algorithm. Besides the novelty of the problem itself, a major technical innovation of this work lies in the fact that the computation mecanism varies along the proof-checking. This is so because the computation operating on propositions is based upon the set of user hypotheses at hand, and therefore evolves with the proof context. Our main result shows that proof-checking remains decidable when considering the congruence closure of the user equational hypotheses on algebraic terms. We also discuss various possible extensions opening quite new interesting perspectives from a theorem proving point of view. In particular, we discuss in more details how the present work can be generalized to the case where the notion of computation is based on Shostak's algorithm for combining decision procedures for convex theories.