coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Polishing commits r14492, r14448 and r14407 (tactics propagate	herbelin	2011-09-25
*	Fix unification: detect invalid evar instantiations due to scoping earlier.	msozeau	2011-08-04
*	Add printer dependency to Hashtbl_alt (used in Term)	puech	2011-07-29
*	Fixed a "feature" of "inversion" and "dependent rewrite" revealed by	herbelin	2011-07-18
*	Finally, pr_goal seems to work for printing v8.2 style goal in debugger.	herbelin	2011-07-16
*	Cleaning debugging printer relative to new proof engine. In	herbelin	2011-06-21
*	A few comments and a dev file to summarize issues with unification	herbelin	2011-06-13
*	A new mechanism to handle errors.	aspiwack	2011-05-13
*	As many notation for for vectors as for List.	pboutill	2011-05-03
*	dev/base_include: no more mod_self_id	letouzey	2011-04-26
*	- Remove create_evar_defs	msozeau	2011-04-13
*	Fix dev/base_include after change of constant_body	letouzey	2011-04-06
*	Adapt printers.mllib after my last commit	letouzey	2011-03-16
*	Annotations at functor applications:	letouzey	2011-02-11
*	Update changelogs	glondu	2011-02-11
*	Factorize code of rewrite to make way for a new implementation using the	msozeau	2011-02-07
*	Remove obsolete script univdot, update dev doc about universes	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Prepare change of nomenclature rawconstr -> glob_constr	glondu	2010-12-23
*	Print universes in debugging printers	glondu	2010-11-08
*	Delayed the evar normalization in error messages to the last minute	herbelin	2010-11-07
*	Remove Explain* vernacs	glondu	2010-10-06
*	Install a printer for fconstr (ppconstr was installed twice)	glondu	2010-10-04
*	Simplify tactic(_)-bound arguments in TACTIC EXTEND rules	glondu	2010-09-30
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	dev/Makefile.oug: how to run the Oug analyser, for instance for finding dead ...	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Updated COPYRIGHT file and header. Improved and fixed header updater.	herbelin	2010-07-24
*	Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).	herbelin	2010-07-22
*	Turned off Mac dynlink hack for 10.6.3+ on x86_64	thutchin	2010-07-05
*	Made tclABSTRACT normalize evars before saying it does not support	herbelin	2010-06-29
*	Names: remove obsolete mod_self_id	letouzey	2010-06-23
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Quick fix for having clenv debug printer working in trunk.	herbelin	2010-06-18
*	Fixed commit 13125 (stricter check of induction args): an interpretation	herbelin	2010-06-14
*	Fixed a bug in pretty-printing "induction" and "destruct" due to a	herbelin	2010-06-13
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Added debugging printer for the idmap used at evar definition time for	herbelin	2010-06-12
*	Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.	herbelin	2010-06-09
*	Replace ld by gcc in ocamlopt_shared_os5fix.sh (Closes: #2325)	glondu	2010-06-07
*	Updated performance analysis file	herbelin	2010-06-06
*	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
*	Improved the efficiency of evars traverals thanks to a split of	herbelin	2010-05-13
*	ocamldoc related fixes	pboutill	2010-05-03
*	"make source-doc" builds documentation of mli in html and pdf at	pboutill	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Removing redundant internal variants of apply tactic and simplification of ML...	herbelin	2010-04-14