coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	A uniformization step around understand_* and interp_* functions.	herbelin	2013-05-09
*	Revert "remove -rectypes except for term.ml"	mdenes	2013-01-22
*	remove -rectypes except for term.ml	letouzey	2012-10-06
*	Remove broken makefile option NO_RECOMPILE_LIB	letouzey	2012-09-20
*	Some documentation of recent changes concerning interfaces	letouzey	2012-05-29
*	debugging.txt: no more typing of #use "include" if using .ocamlinit	letouzey	2011-10-15
*	Moved to a more standard order of arguments (i.e. env followed by evar_map)	herbelin	2011-10-11
*	Moving never-used comments from Zhints.v to dev/doc so as not to	herbelin	2011-10-01
*	A few comments and a dev file to summarize issues with unification	herbelin	2011-06-13
*	Update changelogs	glondu	2011-02-11
*	Remove obsolete script univdot, update dev doc about universes	glondu	2010-12-24
*	Simplify tactic(_)-bound arguments in TACTIC EXTEND rules	glondu	2010-09-30
*	Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).	herbelin	2010-07-22
*	Made tclABSTRACT normalize evars before saying it does not support	herbelin	2010-06-29
*	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
*	Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.	herbelin	2010-06-09
*	Updated performance analysis file	herbelin	2010-06-06
*	Improved the efficiency of evars traverals thanks to a split of	herbelin	2010-05-13
*	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
*	Few misc. updates.	herbelin	2010-01-04
*	Addition of mergesort + cleaning of the Sorting library	herbelin	2009-12-13
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Fixed clash names in Relations (see bug report #2152) and make names	herbelin	2009-10-08
*	Mise à jour du document de révision de la stdlib et déplacement de la	herbelin	2009-08-14
*	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin	2009-08-06
*	Moved and completed the history of Coq versions from the	herbelin	2009-05-24
*	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin	2009-05-09
*	- Cleaning (unification of ML names, removal of obsolete code,	herbelin	2009-04-27
*	Correction du patch -rectypes pour ocaml 3.10	vsiles	2009-04-14
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey	2009-03-20
*	Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)	herbelin	2009-03-17
*	Cleaning/uniformizing the interface of tacticals.mli	herbelin	2009-03-14
*	#rectypes was already automatically added when using 3.11	herbelin	2009-02-17
*	Made hack to have Drop and #use"include" working with ocaml 3.10 public	herbelin	2009-02-17
*	Document how FIND_VCS_CLAUSE has to be used	lmamane	2009-02-11
*	- Structuring Numbers and fixing Setoid in stdlib's doc.	herbelin	2009-01-19
*	- Added support for subterm matching in SearchAbout.	herbelin	2008-12-29
*	About "apply in":	herbelin	2008-12-09
*	Use $(COQTOPEXE) to refer to bin/coqtop in Makefiles	glondu	2008-09-06
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	MAJ diverses	herbelin	2008-06-11
*	- Patch sur "intros until 0"	herbelin	2008-06-08
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	Fix typos	lmamane	2008-06-05
*	- Correction bug highlighting "Module" dans Coqide	herbelin	2008-05-28
*	Mise en place d'un algorithme d'inversion des contraintes de type lors	herbelin	2008-05-05