coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Remove an ununsed pattern and commented code in the kernel.	Matthieu Sozeau	2014-10-24
\| \| \| \| \|	Reestablish completeness in conversion when Opaque primitive projections are used.
*	Pushing Pierre's factorization of names in goal context printing from	Hugo Herbelin	2014-10-22
\| \| \| \| \| \|	coqide to coqtop. (Joint work with Pierre)
*	A patch for printing "match" when constructors are defined with let-in	Hugo Herbelin	2014-10-20
\| \| \| \| \| \| \| \| \| \| \|	but the internal representation dropped let-in. Ideally, the internal representation of the "match" should use contexts for the predicate and the branches. This would however be a rather significant change. In the meantime, just a hack. To do, there is still an extra @ in the constructor name that does not need to be there.
*	Coqide prints succesive hyps of the same type on 1 line	Pierre Boutillier	2014-09-01
\| \| \| \| \|	This revert somehow f5d7b2b1eda550f5bf0965286d449112acbbadde about "Hypotheses don't respect Barendregt convention".
*	Removing some generic equalities.	ppedrot	2013-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16915 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing useless casts between arrays and lists.	ppedrot	2013-08-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16659 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Merging Context and Sign.	ppedrot	2013-04-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
	1. sorts.ml: A small file utility for sorts; 2. constr.ml: Really low-level terms, essentially kind_of_constr, smart constructor and basic operators; 3. vars.ml: Everything related to term variables, that is, occurences and substitution; 4. context.ml: Rel/Named context and all that; 5. term.ml: derived utility operations on terms; also includes constr.ml up to some renaming, and acts as a compatibility layer, to be deprecated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7