coq - The formal proof system

Age	Commit message (Expand)	Author
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
2008-11-22	- Fixed minor bug #1994 in the tactic chapter of the manual [doc]	herbelin
2008-11-21	fixed problem with r11612	barras
2008-11-05	Better extraction renaming phase (fix #1914 plus other non-reported bugs)	letouzey
2008-11-04	Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)	herbelin
2008-10-27	- Fixed many "Theorem with" bugs.	herbelin
2008-10-23	Open notation for declaring record instances.	msozeau
2008-10-22	Affichage des notations récursives:	herbelin
2008-09-02	avoid small overflows	barras
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-27	Now, -browser option is effective (and compiles)	glondu
2008-07-27	(Partially) Revert previous commit because of FTBFS	glondu
2008-07-27	Add -browser option to configure script	glondu
2008-07-24	Suite commit 11236	notin
2008-07-18	Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...	notin
2008-07-16	Quelques modifications autour du filtrage Ltac:	herbelin