coq - The formal proof system

Age	Commit message (Expand)	Author
2010-02-15	Util.lowercase_unicode: avoid creating the segmenttree each time (speeds some...	letouzey
2010-02-10	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau
2010-01-08	* Segmenttree: New. A very simple implementation of segment trees.	regisgia
2009-12-21	Generic support for open terms in tactics	herbelin
2009-12-20	* Rewrite [classify_unicode] using standard unicode tables.	regisgia
2009-11-27	Added support for definition of fixpoints using tactics.	herbelin
2009-11-15	Document Generalizable Variables, and change syntax to	msozeau
2009-11-13	Make usages of the Obj module explicit	glondu
2009-11-12	Experiment propagation of implicit arguments and arguments scope for	herbelin
2009-10-29	Revision 12439 continued, printing part (notations to names behave	herbelin
2009-10-29	Fix bug in dnet.ml, which missed some results when filtering one term against...	puech
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-10-26	New functors for gmap and gset.	soubiran
2009-10-21	This big commit addresses two problems:	soubiran
2009-10-04	Changed the way to support compatibility with previous versions.	herbelin
2009-09-26	Fixed a hole in glob_tactic that allowed some Ltac code to refer to	herbelin
2009-09-22	Add the option to automatically introduce variables declared before the	msozeau
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-11	Generalized the possibility to refer to a global name by a notation	herbelin
2009-08-14	Tried to make F1 documentation tool working in CoqIDE.	herbelin
2009-08-06	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin
2009-07-20	Use camlp4 to accept some specific non-exhaustive patterns in groebner	letouzey
2009-07-08	Fixed anomaly when trying to load non existing file starting with "./" or "../".	herbelin
2009-06-10	Accept more Unicode symbols	glondu
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin
2009-04-27	- Cleaning (unification of ML names, removal of obsolete code,	herbelin
2009-04-16	comparison functions on lists and arrays	barras
2009-04-08	Some dead code removal + cleanups	letouzey
2009-04-08	A first pearl found by the Oug analyzer: there were two list_map_i in Util	letouzey
2009-03-20	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey
2009-03-04	Timeout message was not always displayed	barras
2009-03-02	Heavy modifications on the widget and edition tab creation mechanism.	vgross
2009-02-11	Gestion des espaces dans les noms + guess_coqlib sous Windows	notin
2009-02-11	Fix d'un problème lors de l'appel à coqtop avec un chemin relatif	notin
2009-02-09	memoized is_ground_env	barras
2009-01-27	- Fixed various Overfull in documentation.	herbelin
2009-01-23	Petit nettoyage faisant suite au commit #11847 .	aspiwack
2009-01-22	Util.split_at : for quadratic to linear complexity	letouzey
2009-01-19	Experimental file commited by mistake, sorry.	herbelin
2009-01-18	Backporting from v8.2 to trunk:	herbelin
2009-01-17	DISCLAIMER	puech
2009-01-08	Remove trailing newlines in outputs of X -where	glondu
2009-01-02	Made the debugger work again:	herbelin
2008-12-30	- Fixed bugs and compatibilities issues in	herbelin
2008-12-28	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin
2008-12-24	- coq_makefile: target install now respects the original tree structure	herbelin
2008-12-19	Nettoyage des variables Coq et amélioration de coqmktop. Les	notin
2008-12-15	Add some unicode symbols from japanese CJC (request by Y. Regis-Gianas)	letouzey
2008-11-24	eventually fixing r11612	barras
2008-11-22	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin