coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	CoqIDE: correclty unfocus (remove all tags) when jumping out of a proof	Enrico Tassi	2015-02-25
\|
*	Fix some typos in comments.	Guillaume Melquiond	2015-02-23
\|
*	Fixing bug #4073.	Pierre-Marie Pédrot	2015-02-20
\|
*	Remove Whelp commands.	Maxime Dénès	2015-02-17
\| \| \| \| \| \|	Although these commands were never deprecated, they have been unusable for some time now, since they send requests to an Italian server which is no longer alive.
*	Fixing bug #4023 again.	Pierre-Marie Pédrot	2015-02-17
\|
*	Tentative fix for bug #2855.	Pierre-Marie Pédrot	2015-02-17
\|
*	CoqIDE: read-only Qed sentence reflected in colors (Close: 4051)	Enrico Tassi	2015-02-17
\|
*	Fixing bug #4037.	Pierre-Marie Pédrot	2015-02-15
\|
*	Changing default for CoqIDE project to append arguments.	Pierre-Marie Pédrot	2015-02-15
\| \| \| \|	Implement wish #3582.
*	CoqIDE now remembers the path of the last opened project.	Pierre-Marie Pédrot	2015-02-15
\| \| \| \|	Fixes bug #2762.
*	Selecting whole words on double-click in CoqIDE.	Pierre-Marie Pédrot	2015-02-15
\| \| \| \|	Fixes bug #4026.
*	CoqIDE: restore old default colors	Enrico Tassi	2015-02-14
\|
*	Attempt to be more colorblind friendly in CoqIDE (Close #4024)	Enrico Tassi	2015-02-14
\|
*	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.
*	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.
*	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.
*	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.
*	Fixing bug #4023.	Pierre-Marie Pédrot	2015-02-12
\|
*	Reinstauring backtrace display in CoqIDE.	Pierre-Marie Pédrot	2015-02-11
\|
*	Making undo/redo atomic in CoqIDE.	Pierre-Marie Pédrot	2015-02-10
\|
*	More efficient Richpp.	Pierre-Marie Pédrot	2015-02-06
\| \| \| \|	We build the rich XML at once without generating the printed string.
*	Fixing bug #3996.	Pierre-Marie Pédrot	2015-02-04
\|
*	Made the CoqIDE progress gutter clickable.	Pierre-Marie Pédrot	2015-01-29
\|
*	Made replacing of text in CoqIDE atomic w.r.t. the undo/redo.	Pierre-Marie Pédrot	2015-01-25
\|
*	Fixing bug #3947.	Pierre-Marie Pédrot	2015-01-25
\|
*	CoqIDE: a Make file to build coqidetop toploop	Enrico Tassi	2015-01-14
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Removing GUtil dependency from ide/document.ml.	Pierre-Marie Pédrot	2015-01-05
\| \| \| \|	We reimplement a quick-n-dirty Gtk-free signal handler.
*	Adding an option to deactivate the progress bar.	Pierre-Marie Pédrot	2015-01-05
\|
*	Implementing a segment-viewer in CoqIDE.	Pierre-Marie Pédrot	2015-01-05
\| \| \| \| \| \| \|	This allows a nifty display of the current state of the document through a dedicated progress bar. Also closes bug #3764.
*	CoqIDE: cleanup jobs window on worker death	Enrico Tassi	2014-12-17
\|
*	CThread: use a different type for thread friendly in_channels	Enrico Tassi	2014-12-17
\|
*	CoqIDE: better messages	Enrico Tassi	2014-12-17
\|
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Instead of modifying exceptions to wear additional information, we instead use a dedicated type now. All exception-using functions were modified to support this new type, in particular Future's fix_exn-s and the tactic monad. To solve the problem of enriching exceptions at raise time and recover this data in the try-with handler, we use a global datastructure recording the given piece of data imperatively that we retrieve in the try-with handler. We ensure that such instrumented try-with destroy the data so that there may not be confusion with another exception. To further harden the correction of this structure, we also check for pointer equality with the last raised exception. The global data structure is not thread-safe for now, which is incorrect as the STM uses threads and enriched exceptions. Yet, we splitted the patch in two parts, so that we do not introduce dependencies to the Thread library immediatly. This will allow to revert only the second patch if ever we switch to OCaml-coded lightweight threads.
*	Revert "Fixing bug #3817."	Pierre-Marie Pédrot	2014-12-14
\| \| \| \|	This reverts commit ad2a0308b1592c7235714a2cca926f3b55accbb2.
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
\|
*	Protecting from a List.nth when applying a command, e.g. C-w, on no CoqIDE ↵	Hugo Herbelin	2014-12-07
\| \| \| \|	buffer.
*	Ensuring that ide_slave and stm receive only .v files from CoqIDE.	Hugo Herbelin	2014-12-07
\| \| \| \| \| \|	In particular, renouncing to original support for existing non .v files in CoqIDE (hoping it is ok for anyone). Please amend if better to propose.
*	Remove dead code	Enrico Tassi	2014-12-01
\|
*	Feedback: API cleaned up, documented and made user extensible	Enrico Tassi	2014-11-27
\|
*	Fixing bug #3817.	Pierre-Marie Pédrot	2014-11-24
\| \| \| \| \| \| \| \|	Coqtop was wrongly assuming that receiving a SIGINT when reading on a channel meant that the channel was closed, resulting in a crash when interrupting an idle coqtop from CoqIDE. To prevent this, we block SIGINTs when reading in ide_slave.
*	Reworking the -color flag of coqtop.	Pierre-Marie Pédrot	2014-11-15
\|
*	Fixing compilation (name of module Richprinter) I partially feel	Hugo Herbelin	2014-11-06
\| \| \| \|	responsible about.
*	ide/Xmlprotocol: Cosmetics.	Yann Régis-Gianas	2014-11-04
\|
*	ide/Ide_slave.annotate: Implement annotate.	Regis-Gianas	2014-11-04
\|
*	ide/{ide_slave.ml, interfaces}: Coerce input and output of requests between ↵	Regis-Gianas	2014-11-04
\| \| \| \|	internal and external datatypes.
*	ide/wg_ProofView: Do not refer to the {Proof} internal module, use ↵	Regis-Gianas	2014-11-04
\| \| \| \|	{Interface} instead.