coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix #6798: coqchk ignores ugraph when comparing constant instances	Gaëtan Gilbert	2018-04-20
\|
*	[api] Deprecate a couple of aliases that we missed.	Emilio Jesus Gallego Arias	2018-03-28
\|
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	checker: cleanup projection unfolding	Gaëtan Gilbert	2018-02-02
\| \| \| \|	This just shares the unfold_projection between Closure and Reduction.
*	checker: remove unused per-constant reduction flags.	Gaëtan Gilbert	2018-02-02
\|
*	Actually use the strategy information in the checker.	Pierre-Marie Pédrot	2018-01-14
\|
*	Remove redundant Zcase from the checker.	Pierre-Marie Pédrot	2017-12-02
\| \| \| \| \| \|	This was redundant with ZcaseT, the only difference lying in the use or not of fclosures for substerms. This code was removed from the kernel in commit f2f805ed, we finish the work in the checker now.
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
\| \| \| \|	This will allow to merge back `Names` with `API.Names`
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Correct coqchk reduction	Amin Timany	2017-06-16
\|
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Checker: Fix bug #4282	Matthieu Sozeau	2015-07-07
\| \| \| \| \|	Adapt to new [projection] abstract type comprising a constant and a boolean.
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	improve efficiency of the reduction interpreter of the checker	Bruno Barras	2015-01-06
\| \| \| \| \| \| \|	Conflicts: checker/closure.ml checker/closure.mli checker/reduction.ml
*	Rename eta_expand_ind_stacks, fix the one from the checker and adapt	Matthieu Sozeau	2014-09-05
\| \| \| \| \|	it to the new representation of projections and the new mind_finite type.
*	Adapt the checker to polymorphic universes and projections (untested).	Matthieu Sozeau	2014-05-08
\|
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
\| \| \| \| \| \| \| \|	With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
*	Checker: regroup all vo-related types in cic.mli	letouzey	2013-04-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16398 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modulification of identifier	ppedrot	2012-12-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	checker: add eta-expansion	glondu	2011-03-04
\| \| \| \| \| \|	Backport of changes introduced in r13443 and r13494. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13866 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
\| \| \| \| \| \| \| \| \| \|	conversion. - Fix trans_fconv* to use evars correctly. - Normalize the goal with respect to evars before rewriting in [rewrite], allowing to see instanciations from other subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Checker: remove some dead code	letouzey	2010-09-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13462 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
*	After the approval of Bruno, here the patch for the checker.	soubiran	2010-04-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In checker: - delta_resolver inferred by the module system is checked through regular delta reduction steps - the old mind_equiv field of mutual_inductive is simulated through a special table in environ - small optimization, if the signature and the implementation of a module are physically equal (always happen for the toplevel module of a vo) then the checker checks only the signature. In kernel - in names i have added two special equality functions over constant and inductive names for the checker, so that the checker does not take in account the cannonical name inferred by the module system. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12977 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
\| \| \| \| \| \| \| \| \| \| \|	- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	added the .vo checker (with independent Makefile)	barras	2008-04-21
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10826 85f007b7-540e-0410-9357-904b9bb8a0f7