coq - The formal proof system

Age	Commit message (Expand)	Author
2010-07-22	Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).	herbelin
2010-07-05	Turned off Mac dynlink hack for 10.6.3+ on x86_64	thutchin
2010-06-29	Made tclABSTRACT normalize evars before saying it does not support	herbelin
2010-06-23	Names: remove obsolete mod_self_id	letouzey
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-06-18	Quick fix for having clenv debug printer working in trunk.	herbelin
2010-06-14	Fixed commit 13125 (stricter check of induction args): an interpretation	herbelin
2010-06-13	Fixed a bug in pretty-printing "induction" and "destruct" due to a	herbelin
2010-06-12	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-09	Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.	herbelin
2010-06-07	Replace ld by gcc in ocamlopt_shared_os5fix.sh (Closes: #2325)	glondu
2010-06-06	Updated performance analysis file	herbelin
2010-05-19	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-13	Improved the efficiency of evars traverals thanks to a split of	herbelin
2010-05-03	ocamldoc related fixes	pboutill
2010-04-29	"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-22	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack
2010-04-14	Removing redundant internal variants of apply tactic and simplification of ML...	herbelin
2010-04-05	Added a function in typing.ml to solve evars of a constr w/o going back down ...	herbelin
2010-03-04	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-01-28	Remove bashisms	glondu
2010-01-12	Added module sharing support for typeclasses and hints (pri_auto_tactic).	soubiran
2010-01-08	* Segmenttree: New. A very simple implementation of segment trees.	regisgia
2010-01-04	Few misc. updates.	herbelin
2009-12-24	In "simpl c" and "change c with d", c can be a pattern.	herbelin
2009-12-20	* Rewrite [classify_unicode] using standard unicode tables.	regisgia
2009-12-13	Addition of mergesort + cleaning of the Sorting library	herbelin
2009-12-02	Remove interface plugin	glondu
2009-11-13	Remove useless ppevd (which is identical to ppevm)	glondu
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
2009-11-11	Fixed bug #2168 (closing a section may have as side-effect the erasure	herbelin
2009-11-11	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin
2009-11-09	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin
2009-11-08	Fixed "Scheme Equality" when another instance of the scheme on the	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-10-25	Improved the treatment of Local/Global options (noneffective Local on	herbelin
2009-10-21	This big commit addresses two problems:	soubiran
2009-10-08	Fixed clash names in Relations (see bug report #2152) and make names	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-14	Mise à jour du document de révision de la stdlib et déplacement de la	herbelin
2009-08-07	Fixed incorrect optimization in Prettyp.pr_located_qualid introduced	herbelin
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-08-02	Improved parameterization of Coq:	herbelin
2009-05-26	ocamldebug-coq: add some forgotten -I	letouzey
2009-05-24	Moved and completed the history of Coq versions from the	herbelin
2009-05-20	- Fixing declarative mode in presence of high use of Change_evars nodes	herbelin