coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Addressing part 2 of bug report 2377 (removing intrusive warning when	herbelin	2010-09-19
*	Coqdep_boot : misc improvements	letouzey	2010-09-17
*	* By default, load proof terms.	regisgia	2010-08-31
*	* lib/Flags: Replace dont_load_proofs by load_proofs since not loading	regisgia	2010-08-27
*	Rather quick hack to make basic unicode notations available by	herbelin	2010-07-29
*	Fixed a bug introduced (r13316/r13329) in the printing of notations	herbelin	2010-07-29
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Constrintern: unified push_name_env and push_loc_name_env; made	herbelin	2010-07-22
*	Fixed a bug in list_forall2eq (wrong exception was caught).	herbelin	2010-07-20
*	Remove dependency to Unix from module Profile	glondu	2010-07-02
*	Move [delayed] to util and use [force_delayed] everywhere to force	msozeau	2010-06-30
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Protection against anomaly when loading a state with bad magic number.	herbelin	2010-06-22
*	Extraction: replace unicode characters in ident by ascii encodings (fix #2158...	letouzey	2010-06-21
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Made option "Automatic Introduction" active by default before too many	herbelin	2010-06-08
*	Fix treatment of {struct x} annotations in presence of generalized	msozeau	2010-06-08
*	restore handling of lexer errors	letouzey	2010-06-01
*	CoqIDE goes multiprocess	vgross	2010-05-31
*	Account for Stephane Glondu's remarks.	fkirchne	2010-05-28
*	Use existing functions to reimplement search_exe.	fkirchne	2010-05-28
*	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
*	Various minor improvements of comments in mli for ocamldoc	letouzey	2010-04-29
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Added a new exception for already declared Schemes,	vsiles	2010-04-27
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).	herbelin	2010-04-19
*	Util: remove list_split_at which is a clone of list_chop	letouzey	2010-04-16
*	Look for csdp in $PATH at runtime, remove -csdpdir configure option	glondu	2010-04-11
*	infrastructure for safe marshal-based IPC	vgross	2010-03-23
*	Util.lowercase_unicode: avoid creating the segmenttree each time (speeds some...	letouzey	2010-02-15
*	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau	2010-02-10
*	* Segmenttree: New. A very simple implementation of segment trees.	regisgia	2010-01-08
*	Generic support for open terms in tactics	herbelin	2009-12-21
*	* Rewrite [classify_unicode] using standard unicode tables.	regisgia	2009-12-20
*	Added support for definition of fixpoints using tactics.	herbelin	2009-11-27
*	Document Generalizable Variables, and change syntax to	msozeau	2009-11-15
*	Make usages of the Obj module explicit	glondu	2009-11-13
*	Experiment propagation of implicit arguments and arguments scope for	herbelin	2009-11-12
*	Revision 12439 continued, printing part (notations to names behave	herbelin	2009-10-29
*	Fix bug in dnet.ml, which missed some results when filtering one term against...	puech	2009-10-29
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	New functors for gmap and gset.	soubiran	2009-10-26
*	This big commit addresses two problems:	soubiran	2009-10-21