Constructible DG-modules over the de Rham algebra

Positselski proved that the unbounded derived category of quasi-coherent D-modules on a smooth algebraic variety $X$ is equivalent to a so-called coderived category of quasi-coherent DG-modules over the de Rham algebra of $X$. First I will explain how to work with the coderived category in question. Then I introduce constructible DG-modules. They form a nice subcategory of the coderived category. It turns out that constructible DG-modules correspond to holonomic D-modules under Positselski equivalence.