coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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).
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\|\
\| *	Applying same convention as in Definition for printing type in a let in.	Hugo Herbelin	2017-03-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Also adding spaces around ":=" and ":" when printed as "(x : t := c)". Example: Check fun y => let x : True := I in fun z => z+y=0. (* λ (y : nat) (x : True := I) (z : nat), z + y = 0 : nat → nat → Prop *)
* \|	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot	2017-02-14
\|/ \| \| \| \| \|	Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough.
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\
\| *	Do not give a name to anonymous evars anymore. See bug #4547.	Pierre-Marie Pédrot	2016-02-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The current solution may not be totally ideal though. We generate names for anonymous evars on the fly at printing time, based on the Evar_kind data they are wearing. This means in particular that the printed name of an anonymous evar may change in the future because some unrelate evar has been solved or introduced.
* \|	Adapting output test inference.v after c23f0cab6 (experimenting	Hugo Herbelin	2015-11-08
\|/ \| \| \|	printing the type of the defined term of a LetIn).
*	Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8.	Maxime Dénès	2015-06-24
\|
*	Do not display the status of monomorphic constants unless in ↵	Guillaume Melquiond	2015-03-09
\| \| \| \|	universe-polymorphism mode.
*	Adapting output tests to the removal of the new token warning and to	Hugo Herbelin	2014-10-21
\| \| \| \|	the printing of the context of open evars in Check.
*	Reductionops: (Co)Fixpoints are always refolded during iota	Pierre Boutillier	2014-09-18
\|
*	Fixing output test-suite: since universe polymorphism, the Print command	Pierre-Marie Pédrot	2014-05-08
\| \| \| \|	shows the polymorphism status of the term.
*	Fixing 2 output test-suites.	ppedrot	2013-10-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16863 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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