We present an approach to combine the Coq proof assistant, based on calculus of constructions, with the Elan deduction system, based on rewriting calculus. Our objective is to implement in Coq a class of decision procedures using rewriting techniques. The approach relies on a normalisation tactic in associative and commutative theories that generates a proof term in rewriting calculus, translated into a proof term in calculus of constructions, that can be checked by Coq to get the proof of the normalisation process.