coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	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
\|
*	Win: use .exe extension for the ocaml compiler (Close 3572)	Enrico Tassi	2015-02-11
\|
*	STM: is Flags.async_proofs_full then always delegate	Enrico Tassi	2015-02-11
\| \| \| \| \|	Probably a regression introduced in some code refactoring. Affects only PIDE based code.
*	Fixing bug #4019, and checker blow-up at once.	Pierre-Marie Pédrot	2015-02-11
\|
*	Clarifying the implementation of universe hashconsing.	Pierre-Marie Pédrot	2015-02-11
\|
*	Adding a statistic function on hashconsing tables.	Pierre-Marie Pédrot	2015-02-11
\|
*	Tactic Notation: use stable unique key for notations (Close: 3970)	Enrico Tassi	2015-02-11
\| \| \| \| \|	This is a fixup of commit 2e09a22b that used uniquely generated kernel names but forgot to substitute them.
*	Adding a test-suite for tactic notation naming.	Pierre-Marie Pédrot	2015-02-11
\|
*	Make coqdoc -l properly handle Local before Ltac. (Fix for bug #3307)	Guillaume Melquiond	2015-02-11
\|
*	Adding test for bug #3900.	Pierre-Marie Pédrot	2015-02-11
\|
*	Fixing bug #3900.	Pierre-Marie Pédrot	2015-02-11
\|
*	Reinstauring backtrace display in CoqIDE.	Pierre-Marie Pédrot	2015-02-11
\|
*	Avoid html markup inside tex files and fix url.	Guillaume Melquiond	2015-02-10
\|
*	Run coqdoc on the .v files from the plugins directory. (Fix for bug #2195)	Guillaume Melquiond	2015-02-10
\|
*	Fixing #4001 (missing type constraints when building return clause of match).	Hugo Herbelin	2015-02-10
\|
*	Improving further e11854569b8 and 3e5b9ab9f75e4 on when to print goals in ↵	Hugo Herbelin	2015-02-10
\| \| \| \|	coqtop mode.
*	Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ↵	Hugo Herbelin	2015-02-10
\| \| \| \|	declarations).
*	Fixing #4018 (uncaught exception on non-equality in intros [=]).	Hugo Herbelin	2015-02-10
\|
*	A few refinements in whodidwhat 8.4.	Hugo Herbelin	2015-02-10
\|
*	Fix typeops ignoring results of check functions with let _, and one	Matthieu Sozeau	2015-02-10
\| \| \| \| \| \|	safety hole in judge_of_constant_knowing parameters which was not checking the result of the check correctly (the rest of the calls in that file and all of the checker have been checked).
*	Add section numbering to the refman PDF. (Fix for bug #2365)	Guillaume Melquiond	2015-02-10
\|
*	Prevent Latex from messing with backticks. (Fix for bug #3871)	Guillaume Melquiond	2015-02-10
\|
*	Fix documentation of generalize. (Fix for bug #4015)	Guillaume Melquiond	2015-02-10
\|
*	Fix some documentation typo.	Guillaume Melquiond	2015-02-10
\|
*	Granting wish #4008.	Pierre-Marie Pédrot	2015-02-10
\|
*	Test for bug #4012.	Pierre-Marie Pédrot	2015-02-10
\|
*	More expressive API for tclWITHHOLES.	Pierre-Marie Pédrot	2015-02-10
\|
*	Making undo/redo atomic in CoqIDE.	Pierre-Marie Pédrot	2015-02-10
\|
*	Revert "Removing spurious tclWITHHOLES."	Pierre-Marie Pédrot	2015-02-10
\| \| \| \| \| \| \|	This reverts commit 36c7fba1180eaa2ceea7cc486ebd2f0d649042f0. I had mixed up the boolean flag, resulting in the loss of evar-free versions of tactics.
*	Fix bug #4014.	Pierre-Marie Pédrot	2015-02-09
\|
*	STM: tolerate simple side effects in async proofs (Close: 4006)	Enrico Tassi	2015-02-07
\|
*	Fixing bug #4009.	Pierre-Marie Pédrot	2015-02-07
\| \| \| \|	We only allow color output under Unix OSes.
*	More efficient Richpp.	Pierre-Marie Pédrot	2015-02-06
\| \| \| \|	We build the rich XML at once without generating the printed string.
*	Windows: open .vo files in binary mode	Enrico Tassi	2015-02-05
\|
*	Fix some documentation typos.	Guillaume Melquiond	2015-02-05
\|
*	Fix automatic undo after nonsensical Qed in tty mode (Close: 3980)	Enrico Tassi	2015-02-05
\| \| \| \|	Here nonsensical means a Qed/Defined without a Lemma.
*	Windows installer cleanup	Enrico Tassi	2015-02-05
\|
*	Marshal.from_string on 32 bit systems use tmpfile if needed (Close: 3968)	Enrico Tassi	2015-02-05
\| \| \| \| \| \| \| \|	Strings are at most 16M on 32 bit OCaml, and the system state may be bigger. In this case we write to tmp file and Marshal.from_channel. We can't directly use the channel interface because of badly designed non blocking API (available only on fds and not channels).
*	Properly set module names in presence of -Q. (Fix for bug #3958)	Guillaume Melquiond	2015-02-05
\| \| \| \| \| \| \| \|	This is done by adding a fourth type of loadpath, the ones that are neither implicit nor root, for the subdirectories of a -Q root. Note: this means that scanning for available directories is no longer done on the fly for -Q, but once and for all, as with -R.