coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Extraction: replace unicode characters in ident by ascii encodings (fix #2158...	letouzey	2010-06-21
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12
*	Fix treatment of {struct x} annotations in presence of generalized	msozeau	2010-06-08
*	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-19
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Added a new exception for already declared Schemes,	vsiles	2010-04-27
*	Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).	herbelin	2010-04-19
*	Util: remove list_split_at which is a clone of list_chop	letouzey	2010-04-16
*	Util.lowercase_unicode: avoid creating the segmenttree each time (speeds some...	letouzey	2010-02-15
*	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau	2010-02-10
*	* Segmenttree: New. A very simple implementation of segment trees.	regisgia	2010-01-08
*	* Rewrite [classify_unicode] using standard unicode tables.	regisgia	2009-12-20
*	Document Generalizable Variables, and change syntax to	msozeau	2009-11-15
*	Make usages of the Obj module explicit	glondu	2009-11-13
*	Experiment propagation of implicit arguments and arguments scope for	herbelin	2009-11-12
*	Revision 12439 continued, printing part (notations to names behave	herbelin	2009-10-29
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	Fixed a hole in glob_tactic that allowed some Ltac code to refer to	herbelin	2009-09-26
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Generalized the possibility to refer to a global name by a notation	herbelin	2009-09-11
*	Accept more Unicode symbols	glondu	2009-06-10
*	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin	2009-05-09
*	comparison functions on lists and arrays	barras	2009-04-16
*	A first pearl found by the Oug analyzer: there were two list_map_i in Util	letouzey	2009-04-08
*	Timeout message was not always displayed	barras	2009-03-04
*	Heavy modifications on the widget and edition tab creation mechanism.	vgross	2009-03-02
*	memoized is_ground_env	barras	2009-02-09
*	Petit nettoyage faisant suite au commit #11847 .	aspiwack	2009-01-23
*	Util.split_at : for quadratic to linear complexity	letouzey	2009-01-22
*	Remove trailing newlines in outputs of X -where	glondu	2009-01-08
*	Made the debugger work again:	herbelin	2009-01-02
*	- Fixed bugs and compatibilities issues in	herbelin	2008-12-30
*	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin	2008-12-28
*	- coq_makefile: target install now respects the original tree structure	herbelin	2008-12-24
*	Add some unicode symbols from japanese CJC (request by Y. Regis-Gianas)	letouzey	2008-12-15
*	eventually fixing r11612	barras	2008-11-24
*	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin	2008-11-22
*	fixed problem with r11612	barras	2008-11-21
*	Better extraction renaming phase (fix #1914 plus other non-reported bugs)	letouzey	2008-11-05
*	Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)	herbelin	2008-11-04
*	- Fixed many "Theorem with" bugs.	herbelin	2008-10-27
*	Affichage des notations récursives:	herbelin	2008-10-22
*	avoid small overflows	barras	2008-09-02
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Suite commit 11236	notin	2008-07-24
*	Quelques modifications autour du filtrage Ltac:	herbelin	2008-07-16
*	Fixes in handling of implicit arguments:	msozeau	2008-07-04
*	- Correction de la version simplifiée (filtrage sur deux sig	herbelin	2008-06-09
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08