We propose to use didactical theory for the design of educational software. Here we present a set of didactical conditions, and explain how they shape the software design of Cabri-Euclide, a microworld used to learn "mathematical proof" in a geometry setting. The aim is to design software that does not include a predefined knowledge of problem solution. Key features of the system are its ability to verify local coherence, and not to apply any global and automatic deduction.