coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	Add a new vernacular command for controling implicit generalization of	msozeau	2009-10-27
*	Removal of trailing spaces.	serpyc	2009-10-04
*	kills the old backtracking framework and replaces it with	vgross	2009-09-29
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Ajout de la gestion de Local et Global pour les options (au sens de	aspiwack	2009-08-14
*	Added "etransitivity".	herbelin	2009-08-03
*	Improved parameterization of Coq:	herbelin	2009-08-02
*	remove some unused functions (which are part of a soon-to-be obsolete	vgross	2009-06-22
*	Simplifying the call to print_no_goals and not calling it when no goal	herbelin	2009-06-11
*	Partial simplification of undo mechanism, relying only on Courtieu's	herbelin	2009-06-07
*	dead code pruning	vgross	2009-05-27
*	minor bugfixes. CoqIde development will resume soon now ...	vgross	2009-05-13
*	- per session coq command stack	vgross	2009-03-07
*	fixed groebner as a plugin + pattern matching Timeout	barras	2009-03-06
*	Temporary hack to make coqide.byte work (backport r11948) (see #2062)	glondu	2009-03-04
*	Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk	notin	2009-02-11
*	DISCLAIMER	puech	2009-01-17
*	Conversion du fichier 'revision' en un fichier .ml + correction d'un bug dans...	notin	2009-01-06
*	Nettoyage des variables Coq et amélioration de coqmktop. Les	notin	2008-12-19
*	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau	2008-12-14
*	More factorization of inductive/record and typeclasses: move class	msozeau	2008-11-09
*	Native "Declare ML Module" when possible	glondu	2008-10-28
*	Minor fixes related to coqdoc and --interpolate and the dependent	msozeau	2008-10-03
*	- Rebranchement backtrack du langage déclaratif dans Coqide	herbelin	2008-07-18
*	Bug résiduel du backtrack de coqide se produisant lorsque la limite de	herbelin	2008-07-10
*	Encore une suite au 11188/11193 (c'était pas un bon jour)	herbelin	2008-07-01
*	CoqIDE: 2 problèmes de undo encore:	herbelin	2008-06-13
*	Plutôt que de reposer sur le vernacexpr pour détecter les débuts de	herbelin	2008-06-11
*	On prend des risques en tentant d'optimiser encore plus le undo en cas	herbelin	2008-06-09
*	- On adopte finalement la méthode de Pierre Courtieu pour le undo de	herbelin	2008-06-06
*	- Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"	herbelin	2008-05-30
*	Réorganisation fenêtre d'accueil CoqIDE et About; nouvelle image de	herbelin	2008-05-28
*	Réorganisation des points d'appui du undo de CoqIDE (type reset_info).	herbelin	2008-05-26
*	Bug undo CoqIDE sur End	herbelin	2008-05-26
*	- Nouvelle option "Set Printing Existential Instances" pour forcer	herbelin	2008-05-25
*	- Prise en compte des frozen state de Coq autant que possible pour	herbelin	2008-05-24
*	Léger backtrack sur commit coqide précédent (si la commande à annuler	herbelin	2008-05-20
*	Amélioration de la colorisation, du backtrack et des messages de CoqIDE	herbelin	2008-05-10
*	Efficacité, bugs, robustesse CoqIDE	herbelin	2008-05-08
*	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin	2008-04-25
*	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack	2007-12-06
*	add visibility of extraction messages in coqide	letouzey	2007-10-16
*	Bug 1716: Scheme now print the right messages	vsiles	2007-10-04
*	fin des conclusions multiples	corbinea	2007-04-26
*	New keyword "Inline" for Parameters and Axioms for automatic	soubiran	2007-04-25
*	decl mode: anonymous facts	corbinea	2007-01-25
*	fixed same_file (#1141)	barras	2006-10-23
*	coqide: affichage des sous-buts et hypothèses et métas comme types de	herbelin	2006-10-19