This is an update of the original project GeometricAlgebra.
The project should now be compatible with Coq 8.12.0.
Simply run make to compile the relevant files.
This is the content of the old Readme:
This archive contains all the material of the formalisation of our Grassman Cayley and Clifford formalisation. It has been developped with Coq 8.3 To compile it, a simple make should be enough