coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Generalizing flag use_evars_pattern_unification into a flag	herbelin	2011-06-18
*	Made the emacs-U option deprecated. Also removed the old code	courtieu	2011-05-24
*	Remove useless "open Gc"	glondu	2011-05-19
*	Remove System.process_time (dead code)	glondu	2011-05-19
*	More work on error handling	letouzey	2011-05-17
*	A new mechanism to handle errors.	aspiwack	2011-05-13
*	Choose relative directory over configured directory for coqlib.	pboutill	2011-04-29
*	coqtop -config returns coq returns coq environments at exection time	pboutill	2011-04-28
*	Win32: remove the need for Coq.bat and Coqide.bat	letouzey	2011-04-21
*	Add directories in COQPATH to search path.	herbelin	2011-04-14
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	Starting being more explicit on the reasons why module subtyping fails.	herbelin	2011-03-05
*	- Fix treatment of globality flag for typeclass instance hints (they	msozeau	2011-02-14
*	An generic imperative union-find, used for deps of evars in Class_tactics	letouzey	2011-02-11
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	Fix compilation with camlp5 (Closes: #2487)	glondu	2011-01-25
*	Remove Safe_marshal	glondu	2011-01-06
*	Avoid "open {Pcoq,Extrawit}" clauses in expansion of EXTEND commands	glondu	2010-12-25
*	Use !Pp_control.std_ft for printing grammars	glondu	2010-12-06
*	Remove dead code	glondu	2010-12-03
*	adapt slighlty r13642 to support both camlp4 and camlp5-5 and camlp5-6	letouzey	2010-11-18
*	Support for camlp5 6.02.0 (Closes: #2432)	glondu	2010-11-16
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	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