coq - The formal proof system

Age	Commit message (Collapse)	Author
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-27	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau
	so as to reproduce correctly the reduction behavior of existing projections, i.e. delta + iota. Make [projection] an abstract datatype in Names.ml, most of the patch is about using that abstraction. Fix unification.ml which tried canonical projections too early in presence of primitive projections.
2014-09-26	Add missing "Fail" to bug cases.	Xavier Clerc

2014-09-25	Add several reproduction files for bugs.	Xavier Clerc