We propose the basis of a higher-order logical framework to axiomatize and build proofs in Hilbert’s elementary geometry in
which intuitionistic aspects are emphasized. More precisely, we use the Calculus of inductive constructions and the system
Coq to specify geometric concepts and to study and interactively handle proofs for the first two groups of Hilbert’s axiomatics.
It is the first step to a formalization well adapted to the definition of primitive operations that are used in many different
geometric algorithms.