We show the equivalence between the so-called Davis-Putnam procedure (Davis et al., Comm. ACM 5 (1962) 394-397; Davis and Putnam (J. ACM 7 (1960) 201-215)) and the Forward Checking of Haralick and Elliot (Artificial Intelligence 14 (1980) 263-313). Both apply the paradigm choose and propagate in two different formalisms, namely the propositional calculus and the constraint satisfaction problems formalism. They happen to be strictly equivalent as soon as a compatible instantiation order is chosen. This equivalence is shown considering the resolution of the clausal expression of a CSP by the Davis-Putnam procedure.