coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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