coq - The formal proof system

Age	Commit message (Expand)	Author
2010-06-03	plugin groebner updated and renamed as nsatz; first version of the doc of nsa...	pottier
2010-06-02	Fix xml test in non-local mode	glondu
2010-06-02	Do not link system library into installed .cma	glondu
2010-06-02	Fix typos	glondu
2010-06-02	Fix test-suite cleaning	glondu
2010-06-02	Extraction: start of a support library	letouzey
2010-06-01	added -args option to coqide to pass options to coqtops	vgross
2010-06-01	Cleanup: remove code specific for ocaml 3.06	letouzey
2010-06-01	restore handling of lexer errors	letouzey
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-29	New pass on inductive schemes	herbelin
2010-05-29	Typo in comment of proof.ml	herbelin
2010-05-28	A little bit of cleanup, and some annotations.	fkirchne
2010-05-28	Account for Stephane Glondu's remarks.	fkirchne
2010-05-28	Modify the test for csdp and associated message.	fkirchne
2010-05-28	Use existing functions to reimplement search_exe.	fkirchne
2010-05-28	...	fkirchne
2010-05-28	Correction program_simplify. Devrait corriger certaines contribs.	aspiwack
2010-05-28	Generalized the formulation of classic_set in propositional contexts	herbelin
2010-05-28	Minor fix in doc chapter on inference rules (added a missing space).	herbelin
2010-05-28	Documentation of pretype_id (minor commit).	herbelin
2010-05-26	Fixing Derive Inversion for new proof engine	herbelin
2010-05-22	Added UIP_dec on suggestion of Eelis on #coq irc.	herbelin
2010-05-21	Extract Inductive is now possible toward non-inductive types (e.g. nat => int)	letouzey
2010-05-20	Added examples for checking that the guard condition excludes subterms	herbelin
2010-05-20	Fix bug 2307	pboutill
2010-05-20	fixed guard check with commutative cuts	barras
2010-05-20	Mrec was not substituted correctly	barras
2010-05-19	Ocamlbuild: various fix	letouzey
2010-05-19	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey
2010-05-19	Nicer representation of tokens, more independant of camlp*	letouzey
2010-05-19	Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a naive way	letouzey
2010-05-19	static (and shared) camlp4use instead of per-file declaration	letouzey
2010-05-19	Discontinue support for ocaml 3.09.*	letouzey
2010-05-19	Remove compile-command pragmas for emacs	letouzey
2010-05-18	Some ocamldoc comments + Fixing name of .coqrc.version file in refman	pboutill
2010-05-18	Applicative commutative cuts in Fixpoint guard condition	pboutill
2010-05-13	Improved the efficiency of evars traverals thanks to a split of	herbelin
2010-05-12	Missing warning flush in a lexer message + update of CHANGES	herbelin
2010-05-10	Backporting r13007 (evar_merge wrong and costly) to V8.3 and added test.	herbelin
2010-05-10	Fix: Pfedit.get_current_goal_context when no goal is focused.	aspiwack
2010-05-10	Removed an evar_merge in clenv_fchain which not only is incorrect but	herbelin
2010-05-09	Removed $Id$ introduced inadvertently in r13005 (no more $Id$ since r12972)	herbelin
2010-05-09	Added a few informations about file lineages (for the most part in kernel)	herbelin
2010-05-09	Update of credits files	herbelin
2010-05-07	Fix bug #2315 : printing of defined evars in Coqide.	aspiwack