coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-10-04	rename test files (do not start by a digit)	Vincent Laporte

2014-09-29	In evarconv and unification, expand folded primitive projections to	Matthieu Sozeau
	their eta-expanded forms which can then unfold back to the unfolded primitive projection form. This removes all special code that was necessary to handle primitive projections before, while keeping compatibility. Also fix cbn which was not refolding primitive projections correctly in all cases. Update some test-suite files accordingly.
2014-09-26	Fix canonical structure resolution which was launched on the results of	Matthieu Sozeau
	eta-expansion, creating a loop. This is now deactivated. Fixes bugs #3665 and #3667.