coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix ill-typed debugging function	Matthieu Sozeau	2014-10-15
*	Adding printers for ppproofview.	Hugo Herbelin	2014-10-13
*	Add debug printers for projections, fix printing of evar constraints	Matthieu Sozeau	2014-10-10
*	Adding printer for named_context_val and Goal.goal in debugger.	Hugo Herbelin	2014-10-09
*	Adding a printer for hints.	Hugo Herbelin	2014-10-07
*	Fixing interpretation of constr under binders which was broken after	Hugo Herbelin	2014-10-02
*	Fixing nice printing of error reporting with ml tactics bound to ltac names.	Hugo Herbelin	2014-10-01
*	Fixing use of arguments renaming in apply which was broken after	Hugo Herbelin	2014-10-01
*	Index keys instead of simply global references.	Matthieu Sozeau	2014-09-27
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	win32: embed NSIS for plugin writers	Enrico Tassi	2014-09-19
*	Fix debug printing with primitive projections.	Matthieu Sozeau	2014-09-18
*	win32: remove outdated splash screen	Enrico Tassi	2014-09-17
*	win32: use subsystem windows on windows (and not console)	Enrico Tassi	2014-09-17
*	Fix base_include due to change in argument order of env and evar_map	Matthieu Sozeau	2014-09-12
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	VernacExtend does not dispatch on type anymore.	Pierre-Marie Pédrot	2014-09-10
*	Merge remote-tracking branch 'jason/win32-improvements' into trunk	Enrico Tassi	2014-09-09
\|\
\| *	Bump CoqSDK revision number	Jason Gross	2014-09-09
\| *	Add a VERBOSE flag to make-sdk-win32	Jason Gross	2014-09-09
\| *	Minor code style cleanup in make-sdk-win32	Jason Gross	2014-09-09
\| *	Support 64-bit cygwin	Jason Gross	2014-09-09
\| *	Support machines that have a full or nonexistant C drive	Jason Gross	2014-09-09
\| *	Support environments where `find` is Windows' find	Jason Gross	2014-09-09
* \|	Installer for win improved	Enrico Tassi	2014-09-09
\|/
*	Installer for win32	Enrico Tassi	2014-09-09
*	Debug RAKAM	Pierre Boutillier	2014-08-26
*	A reorganization of the "assert" tactics (hopefully uniform naming	Hugo Herbelin	2014-08-18
*	Reorganisation of intropattern code	Hugo Herbelin	2014-08-18
*	Fixing include of debugger.	Pierre-Marie Pédrot	2014-08-18
*	STM: encapsulate Pp.message in Feedback.feedback	Carst Tankink	2014-08-04
*	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin	2014-08-01
*	Moved code for finding subterms (pattern, induction, set, generalize, ...)	Hugo Herbelin	2014-06-28
*	Made the subterm finding function make_abstraction independent of the	Hugo Herbelin	2014-06-28
*	More open in base_include	Hugo Herbelin	2014-06-28
*	all coqide specific files moved into ide/	Enrico Tassi	2014-06-25
*	Dummy commit to test the new setup of coq-commits mailinglist (bis)	Pierre Letouzey	2014-06-17
*	Dummy commit to test the new setup of coq-commits mailinglist	Pierre Letouzey	2014-06-17
*	Change Ltac constr matching semantics to consider universes when merging two	Matthieu Sozeau	2014-06-15
*	- Fix bug #3368, due to wrong use of the Cst_stack for projections.	Matthieu Sozeau	2014-06-11
*	Fix module order in printers.mllib	Matthieu Sozeau	2014-06-10
*	Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...	Matthieu Sozeau	2014-06-10
*	Moving a Thread.yield in check_interrupt.	Pierre-Marie Pédrot	2014-06-07
*	Adding a new Control file centralizing the control options of Coq.	Pierre-Marie Pédrot	2014-06-07
*	A little bit of documentation about V5.10 and V6.3 and V7.	Hugo Herbelin	2014-06-01
*	- Fix in kernel conversion not folding the universe constraints	Matthieu Sozeau	2014-05-26
*	Isolating a function "make_abstraction", new name of "letin_abstract",	Hugo Herbelin	2014-05-08
*	Renaming new_induct -> induction; new_destruct -> destruct.	Hugo Herbelin	2014-05-08
*	Moving Dnet-related code to tactics/.	Pierre-Marie Pédrot	2014-05-08