coq - The formal proof system

Age	Commit message (Expand)	Author
2010-09-24	Fixed a bug in printing fix/cofix error messages when several	herbelin
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-09-18	Fixing #2162 and #2367 (wrong order of Show Match) for branch 8.2 too	herbelin
2010-09-18	Fixing bugs #2347 (part 2) and #2388: error message printing was done	herbelin
2010-09-14	CoqIDE argv parsing delegated to coqtop	vgross
2010-09-13	Fix unescaped end-of-lines (OCaml warning 29)	glondu
2010-09-02	* removed declare_constant and declare_internal_constant	vsiles
2010-09-02	v13392 port from v8.3 to trunk : correct message when defining inductive schemes	vsiles
2010-08-31	* By default, load proof terms.	regisgia
2010-08-27	* scripts/Coqc toplevel/Usage:	regisgia
2010-08-27	* toplevel/Coqtop: Reactivate -dont-load-proofs option.	regisgia
2010-08-27	* lib/Flags: Replace dont_load_proofs by load_proofs since not loading	regisgia
2010-08-26	Fix an error message ot having the ERror: prefix.	courtieu
2010-07-29	Rather quick hack to make basic unicode notations available by	herbelin
2010-07-27	Fix computation of fix annotation index: only consider assumptions and	msozeau
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-23	Some fine-tuning after removal of automatic imports of coercions in r13310	herbelin
2010-07-22	Extension of the recursive notations mechanism	herbelin
2010-07-22	Simplified the way internalization_data (i.e. bindings of bound vars	herbelin
2010-07-22	Constrintern: unified push_name_env and push_loc_name_env; made	herbelin
2010-07-16	Amelioration dans Function	jforest
2010-07-05	Fix goal display when backtracking	vgross
2010-07-05	Stronger checks on coqtop termination, warning when zombies.	vgross
2010-06-29	Correct wrong handling of evars in instance definitions that prevented	msozeau
2010-06-29	change the flag "internal" in declare/ind_tables from bool to	vsiles
2010-06-29	Made tclABSTRACT normalize evars before saying it does not support	herbelin
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-06-12	Fixed bug #2135 (second-order unification was raising cryptic message)	herbelin
2010-06-12	Added regression tests for bugs + miscellaneous improvements	herbelin
2010-06-12	Applying François' patch fixing grammar of uniform inheritance condition mes...	herbelin
2010-06-12	Fixing spelling: pr_coma -> pr_comma	herbelin
2010-06-09	Automatic introduction of names given before ":" in Lemma's and	herbelin
2010-06-08	Fix treatment of {struct x} annotations in presence of generalized	msozeau
2010-06-07	fixing error message display.	vgross
2010-06-06	Added support for Ltac-matching terms with variables bound in the pattern	herbelin
2010-06-03	Added command "Locate Ltac qid".	herbelin
2010-06-03	Ide_blob: avoid direct use of Stdpp for compatibility with new camlp4	letouzey
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-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	static (and shared) camlp4use instead of per-file declaration	letouzey
2010-05-19	Remove compile-command pragmas for emacs	letouzey
2010-05-18	Applicative commutative cuts in Fixpoint guard condition	pboutill