coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	no-refold patch	Paul Steckler	2016-09-09
\| \| \| \| \| \|	Add a boolean for refolding during reduction, and an option that is off by default in 8.6, to turn refolding on in all reduction functions, as in 8.5.
*	Continuation of r16346 on filtering local definitions. Refined	herbelin	2013-03-30
\| \| \| \| \| \| \| \| \| \| \| \|	the "choose less dependent" constraint-solving heuristic so that it is not disturbed by local definitions. This is a quick fix. A deeper analysis of the structure of constraints of the form ?x[args] = y, determining if variable y can itself be a local def or not, and whether args can be let-ins aliasing other variables, would allow to know if the fix needs to be refined further. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16376 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Evarconv: When doing a iota of a fixpoint, use constant name instead of ↵	pboutill	2013-02-25
\| \| \| \| \| \| \| \|	fixpoint definition + Help the use of #trace on evar_conv_appr_x git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16244 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A small test for type inference (used to be a regression at some time).	herbelin	2011-12-04
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14759 85f007b7-540e-0410-9357-904b9bb8a0f7