coq - The formal proof system

Age	Commit message (Expand)	Author
2010-06-07	fixing error message display.	vgross
2010-06-01	added -args option to coqide to pass options to coqtops	vgross
2010-05-31	CoqIDE goes multiprocess	vgross
2010-05-31	More indirection.	vgross
2010-05-31	Introducing strong typing for IDE - toplevel IPC	vgross
2010-05-31	deporting Coq specific code from ide to toplevel.	vgross
2010-05-31	Modifying startup sequence	vgross
2010-05-19	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey
2010-05-07	Fix bug #2315 : printing of defined evars in Coqide.	aspiwack
2010-05-05	Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proof	pboutill
2010-04-30	Fail: a way to check that a command is refused without blocking a script	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-22	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack
2010-03-23	Changing types to reflect futur separation between toplevel and ide.	vgross
2010-03-23	Goal generation deported into ide/coq.ml, single function to obtain	vgross
2010-03-23	New functions for goals fetching.	vgross
2010-03-23	Fix bug in backtracking.	vgross
2010-03-23	debugging	vgross
2010-02-26	New backtracking code + fix bug #2082.	vgross
2010-02-26	Introducing a dual stack setup	vgross
2010-02-26	New API for backtracking.	vgross
2010-02-26	Redispatch of printing tweaking hooks.	vgross
2010-02-12	Simplify backtracking	vgross
2010-02-12	Delineating a API for Coq inside toplevel/vernac.ml	vgross
2010-02-12	Refactoring of the printing options	vgross
2010-01-28	New command Declare Reduction <id> := <conv_expr>.	letouzey
2010-01-11	Revert "Isolation of proof-displaying code"	vgross
2010-01-11	Isolation of proof-displaying code	vgross
2009-12-11	Deport the backtracking code out of the ide	vgross
2009-12-08	Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...	letouzey
2009-12-03	Fix bug #2191 : Serious "undo" performance degradation since 8.2pl1	vgross
2009-11-19	Refactoring of coqide backtrack code, with the intent to put everything	vgross
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-27	Add a new vernacular command for controling implicit generalization of	msozeau
2009-10-04	Removal of trailing spaces.	serpyc
2009-09-29	kills the old backtracking framework and replaces it with	vgross
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-14	Ajout de la gestion de Local et Global pour les options (au sens de	aspiwack
2009-08-03	Added "etransitivity".	herbelin
2009-08-02	Improved parameterization of Coq:	herbelin
2009-06-22	remove some unused functions (which are part of a soon-to-be obsolete	vgross
2009-06-11	Simplifying the call to print_no_goals and not calling it when no goal	herbelin
2009-06-07	Partial simplification of undo mechanism, relying only on Courtieu's	herbelin
2009-05-27	dead code pruning	vgross
2009-05-13	minor bugfixes. CoqIde development will resume soon now ...	vgross
2009-03-07	- per session coq command stack	vgross
2009-03-06	fixed groebner as a plugin + pattern matching Timeout	barras
2009-03-04	Temporary hack to make coqide.byte work (backport r11948) (see #2062)	glondu
2009-02-11	Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk	notin