coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix 'don't expose cases' in cbn	Pierre Boutillier	2015-02-15
\|
*	Note about "Undo. Undo." in CHANGES	Enrico Tassi	2015-02-15
\|
*	Test for bug #3490.	Pierre-Marie Pédrot	2015-02-15
\|
*	Fixing bug #3490.	Pierre-Marie Pédrot	2015-02-15
\|
*	Test for bug #3916.	Pierre-Marie Pédrot	2015-02-15
\|
*	Fixing bug #3916.	Pierre-Marie Pédrot	2015-02-15
\|
*	Fixing test-suite.	Pierre-Marie Pédrot	2015-02-15
\|
*	Document the behavior change of Instance wrt {\|...\|}. (Fix for bug #3749)	Guillaume Melquiond	2015-02-15
\|
*	Win: update README	Enrico Tassi	2015-02-14
\|
*	Fixing OCaml 3.12 compilation.	Pierre-Marie Pédrot	2015-02-14
\|
*	CoqIDE: restore old default colors	Enrico Tassi	2015-02-14
\|
*	typo	Enrico Tassi	2015-02-14
\|
*	Attempt to be more colorblind friendly in CoqIDE (Close #4024)	Enrico Tassi	2015-02-14
\|
*	Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior	Enrico Tassi	2015-02-14
\| \| \| \|	Of course such proofs cannot be processed asynchronously
*	Makefile: in byte we can always dynlink	Enrico Tassi	2015-02-14
\|
*	Test for bug #4016.	Pierre-Marie Pédrot	2015-02-14
\|
*	Fixing bug #4016.	Pierre-Marie Pédrot	2015-02-14
\| \| \| \| \|	When setoid rewriting in a hypothesis, we push the newly introduced declaration after the last declaration it depends on.
*	dependent destruction: Fix (part of) bug #3961, by fixing dependent *	Matthieu Sozeau	2015-02-14
\| \| \| \|	generalizing * which was broken since 8.4.
*	coqc accepts -top option. Fixes bug #4043.	Pierre-Marie Pédrot	2015-02-14
\|
*	Univs: fix bug #3755. We were missing refreshements of universes in	Matthieu Sozeau	2015-02-14
\| \| \| \|	unifications ?X ~= ?Y foo not catched by solve_evar_evar.
*	Univs: When computing the level of an inductive including indices, lets	Matthieu Sozeau	2015-02-14
\| \| \| \|	do not contribute. Fixes bug #3808.
*	Document the issue with trivial inductive types. (Workaround for bug #3984)	Guillaume Melquiond	2015-02-13
\|
*	Fixup version & copyright for MacOS bundle	Pierre Boutillier	2015-02-13
\|
*	Hardcode how coqide have to look for coqtop in MacOS bundle	Pierre Boutillier	2015-02-13
\| \| \| \|	Sorry, that is ugly. Please revert if you see a better way to do it.
*	Better error message for nested module application.	Maxime Dénès	2015-02-13
\| \| \| \|	Fixes #3809.
*	Fix test-suite file to finish	Matthieu Sozeau	2015-02-13
\|
*	Selection of the current word in CoqIDE looks at all buffers.	Pierre-Marie Pédrot	2015-02-13
\|
*	Trying to fix bug #3930.	Pierre-Marie Pédrot	2015-02-13
\| \| \| \| \| \|	Instead of setting the last modified part of the text to be the insert point, we register all modifications to the buffer between to user actions and take the last modified point to be the least offset of all those modifications.
*	Fixed test-suite file, that should always work.	Matthieu Sozeau	2015-02-12
\|
*	Add test-suite files for closed bugs.	Matthieu Sozeau	2015-02-12
\|
*	Tentative fix for CoqIDE randomly dropping deletions.	Pierre-Marie Pédrot	2015-02-12
\| \| \| \| \| \|	We make the deletion callback not to regenerate a task id, as the insertion callback does. I can't find a particular reason for this dissymetry, and it was indeed causing trouble.
*	COMPATIBILITY: add note about the change of behavior of Instance foo :=	Matthieu Sozeau	2015-02-12
\| \| \| \|	{\| \|}. Add test-suite files for closed bugs.
*	Univs: fix bug #4031: wrong folding of sigma in change.	Matthieu Sozeau	2015-02-12
\|
*	Univs: fix bug #3978: carry around the universe context used to	Matthieu Sozeau	2015-02-12
\| \| \| \| \|	typecheck with definitions and thread it accordingly when typechecking module expressions.
*	Fix bug #2775: Correct handling of universes in leminv.	Matthieu Sozeau	2015-02-12
\|
*	Fix typos about .vio files (thanks Arthur for spotting them)	Enrico Tassi	2015-02-12
\|
*	Fixing bug #3261.	Pierre-Marie Pédrot	2015-02-12
\|
*	Focussing on message view in CoqIDE when a message is pushed.	Pierre-Marie Pédrot	2015-02-12
\| \| \| \|	Also fixes bug #4030.
*	Revert "Using same code for browsing physical directories in coqtop and coqdep."	Hugo Herbelin	2015-02-12
\| \| \| \| \| \|	(Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
*	Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)	Hugo Herbelin	2015-02-12
\| \| \| \|	This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767.
*	Capital letter in plugins.	Hugo Herbelin	2015-02-12
\|
*	Using same code for browsing physical directories in coqtop and coqdep.	Hugo Herbelin	2015-02-12
\| \| \| \| \| \| \|	In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error).
*	Fixing #3982 (conflict with max notation for universes).	Hugo Herbelin	2015-02-12
\|
*	Fixing #3997 (occur-check in the presence of primitive projections, patch	Hugo Herbelin	2015-02-12
\| \| \| \|	from Matthieu).
*	Fixing bug #4023.	Pierre-Marie Pédrot	2015-02-12
\|
*	Fixing compilation for 3.12.	Pierre-Marie Pédrot	2015-02-12
\|
*	Tentative fix for bug #4027.	Pierre-Marie Pédrot	2015-02-12
\|
*	Make clearer that "Remove Printing Let" does not influence destructuring let.	Guillaume Melquiond	2015-02-12
\|
*	Adding test for bug #3786.	Pierre-Marie Pédrot	2015-02-11
\|
*	Missing space in error message	Matěj Grabovský	2015-02-11
\|