coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	Fix bug #3591: print differently eta-expanded projection implicit application...	Matthieu Sozeau	2014-09-08
*	Parsing of Type@{max(i,j)}.	Matthieu Sozeau	2014-09-08
*	Display number of available goals in "incorrect number of goals" error message.	Arnaud Spiwack	2014-09-08
*	CHANGES: existential variables are always "substituted" in the new tactic eng...	Arnaud Spiwack	2014-09-08
*	CHANGES: Ltac's [refine] accepts [uconstr].	Arnaud Spiwack	2014-09-08
*	Doc: [revgoals].	Arnaud Spiwack	2014-09-08
*	CHANGES: [revgoals].	Arnaud Spiwack	2014-09-08
*	Fix [induction] wrt inductive records and non-recursive variants.	Arnaud Spiwack	2014-09-08
*	CHANGES: [Variant], [Set Nonrecursive Elimination Schemes].	Arnaud Spiwack	2014-09-08