coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-06-07	Put all plugins behind an "API".	Matej Kosik

2017-06-05	Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ↵	Maxime Dénès
	a flag suspectingly renamed in a clearer way
2017-05-31	Using a more explicit algebraic type for evars of kind "MatchingVar".	Hugo Herbelin
	A priori considered to be a good programming style.
2017-05-30	Support for using type information to infer more precise evar sources.	Hugo Herbelin
	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).
2017-04-28	Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"."	Maxime Dénès
	I'm sure this was pushed by accident, since testing shows immediately that it breaks the compilation of the ssreflect plugin, hence all developments relying on it in Travis.
2017-04-28	Using a more explicit algebraic type for evars of kind "MatchingVar".	Hugo Herbelin
	A priori considered to be a good programming style.
2017-01-22	Adding a new evar source to remember the name of evars which were	Hugo Herbelin
	named in the original term. Useful at least for debugging, useful to give a better message than "this placeholder", even if in the loc is known in this case.
2016-01-20	Update copyright headers.	Maxime Dénès

2015-01-12	Update headers.	Maxime Dénès

2014-12-11	Tentatively more informative report of failure when inferring	Hugo Herbelin
	pattern-matching predicate.
2014-12-07	Improved tracking of the origin of evars.	Hugo Herbelin

2014-06-13	Improved error message when a meta posed as an evar remains unsolved	Hugo Herbelin
	in case prefix 'e' of "apply" and co is not given.
2012-12-18	Modulification of name	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14	Modulification of identifier	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08	Updating headers.	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in ↵	letouzey
	grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7