coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- 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
*	Added a function in typing.ml to solve evars of a constr w/o going back down ...	herbelin	2010-04-05
*	Makefile: cleanup of comments + a few words about recent changes in dev/doc/b...	letouzey	2010-03-04
*	Makefile: make devdocclean was not removing .dep.ps, btw let's remove .dep....	letouzey	2010-03-04
*	Remove bashisms	glondu	2010-01-28
*	Added module sharing support for typeclasses and hints (pri_auto_tactic).	soubiran	2010-01-12
*	* Segmenttree: New. A very simple implementation of segment trees.	regisgia	2010-01-08
*	Few misc. updates.	herbelin	2010-01-04
*	In "simpl c" and "change c with d", c can be a pattern.	herbelin	2009-12-24
*	* Rewrite [classify_unicode] using standard unicode tables.	regisgia	2009-12-20
*	Addition of mergesort + cleaning of the Sorting library	herbelin	2009-12-13