coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Replace the list of argument in tacexpr with a single row argument.	Arnaud Spiwack	2014-09-12
*	Oopps.. fixed the .ml not the .ml4	Matthieu Sozeau	2014-09-11
*	Use an AST for strategy names.	Matthieu Sozeau	2014-09-11
*	Fix test-suite files, and move some opened to closed.	Matthieu Sozeau	2014-09-11
*	Add a flag for restricting resolution of typeclasses to	Matthieu Sozeau	2014-09-11
*	Keeping a sub-optimal behavior of intros_possibly_replacing for compatibility...	Hugo Herbelin	2014-09-11
*	Other bugs with "inversion as" (collision between user-provided names and gen...	Hugo Herbelin	2014-09-11
*	Fix bug #3594: eta for constructors and functions at the same time which	Matthieu Sozeau	2014-09-11
*	Fix bug #3596, wrong treatment of projections in compute_constelim_direct.	Matthieu Sozeau	2014-09-11
*	Fix bug #3505.	Matthieu Sozeau	2014-09-11
*	Fixing bug #3605.	Pierre-Marie Pédrot	2014-09-11
*	Removing remaining documentation of the XML plugin.	Pierre-Marie Pédrot	2014-09-11
*	A step towards better differentiating when w_unify is used for subterm	Hugo Herbelin	2014-09-10
*	Parsing and printing of primitive projections, fix buggy behavior when	Matthieu Sozeau	2014-09-10
*	Fix generation of inductive elimination principle for primitive records.	Matthieu Sozeau	2014-09-10
*	Fix categorization of recursive inductives.	Matthieu Sozeau	2014-09-10
*	Fixing localisation of tactic errors (my mistake in himsg.ml essentially).	Hugo Herbelin	2014-09-10
*	More small bugs in intros_replacing.	Hugo Herbelin	2014-09-10
*	Fixing inversion after having fixed intros_replacing	Hugo Herbelin	2014-09-10
*	Example for apply and evars.	Hugo Herbelin	2014-09-10
*	Removing "eqn:" for "induction" in reference manual.	Hugo Herbelin	2014-09-10
*	VernacExtend does not dispatch on type anymore.	Pierre-Marie Pédrot	2014-09-10
*	- Fix printing and parsing of primitive projections, including the Set	Matthieu Sozeau	2014-09-09
*	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
* \|	Displaying genarg tag in idtac.	Pierre-Marie Pédrot	2014-09-09
* \|	Installer for win improved	Enrico Tassi	2014-09-09
\|/
*	IDE: escape popup text (close: 3600)	Enrico Tassi	2014-09-09
*	Load Prelude.vi if not Prelude.vo is found (Close: 3595)	Enrico Tassi	2014-09-09
*	Marshalling errors should be bold and red (should never happen actually)	Enrico Tassi	2014-09-09
*	A marshalling failure does not make a worker `Old	Enrico Tassi	2014-09-09
*	Documenting the new Undo semantics	Enrico Tassi	2014-09-09
*	Back: print subgoals as in 8.4 (Close: 3585)	Enrico Tassi	2014-09-09
*	BackTo not part of the doc when used by emacs	Enrico Tassi	2014-09-09
*	Undo: if the ui is coqtop (command line) then Undo is not part of the doc.	Enrico Tassi	2014-09-09
*	Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)	Enrico Tassi	2014-09-09
*	IDE: disable editable text area underline when -debug	Enrico Tassi	2014-09-09
*	toploop plugins taken into account when printing --help (close: 3535)	Enrico Tassi	2014-09-09
*	Installer for win32	Enrico Tassi	2014-09-09
*	IDECDEPSFLAGS is for byte, not opt	Enrico Tassi	2014-09-09
*	Fixing TestRefine test-suite file.	Pierre-Marie Pédrot	2014-09-08
*	Removing antiquotations in Tauto.	Pierre-Marie Pédrot	2014-09-08
*	Removing dead code relative to the XML plugin.	Pierre-Marie Pédrot	2014-09-08
*	Removing the documentation of the XML plugin.	Pierre-Marie Pédrot	2014-09-08
*	Removing the XML plugin.	Pierre-Marie Pédrot	2014-09-08