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-20	* Rewrite [classify_unicode] using standard unicode tables.	regisgia
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-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-09-26	Fixed a hole in glob_tactic that allowed some Ltac code to refer to	herbelin
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-06-10	Accept more Unicode symbols	glondu
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin
2009-04-16	comparison functions on lists and arrays	barras
2009-04-08	A first pearl found by the Oug analyzer: there were two list_map_i in Util	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-09	memoized is_ground_env	barras
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-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-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-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-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-24	Suite commit 11236	notin
2008-07-16	Quelques modifications autour du filtrage Ltac:	herbelin
2008-07-04	Fixes in handling of implicit arguments:	msozeau
2008-06-09	- Correction de la version simplifiée (filtrage sur deux sig	herbelin
2008-06-08	- Extension de "generalize" en "generalize c as id at occs".	herbelin
2008-06-06	Correction terminologie et ajout plage unicode 1D400-1D7FF (mathematical	herbelin
2008-05-24	Ajout de la possibilité d'utiliser fix/cofix dans les notations.	herbelin
2008-05-15	Various fixes:	msozeau
2008-05-10	- Prise en compte de l'unicode dans la fonction hdchar (elle fournissait des	herbelin
2008-04-14	Diverses corrections	herbelin
2008-04-13	Bugs, nettoyage, et améliorations diverses	herbelin
2008-03-18	improved the implementation of rtree	barras
2008-02-22	Merge with lmamane's private branch:	lmamane
2008-01-30	Add list_iter3	msozeau