coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Deprecate options that were introduced for compatibility with 8.5.	Théo Zimmermann	2017-07-11
\|
*	Support for using type information to infer more precise evar sources.	Hugo Herbelin	2017-05-30
\| \| \| \| \| \| \| \|	This allows a better control on the name to give to an evar and, in particular, to address the issue about naming produced by "epose proof" in one of the comment of Zimmi48 at PR #248 (see file names.v). Incidentally updating output of Show output test (evar numbers shifted).
*	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