coq - The formal proof system

Age	Commit message (Expand)	Author
2009-03-28	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau
2009-03-09	Optionally list opaque constants in addition to axions/variables in	msozeau
2009-03-04	commande Timeout + compaction des traces de debug_tactic	barras
2009-01-19	Les records déclarés avec Record ne peuvent plus être récursifs (le	aspiwack
2009-01-18	Backporting from v8.2 to trunk:	herbelin
2009-01-18	Getting rid of the previous implementation of setoid_rewrite which was	msozeau
2009-01-17	DISCLAIMER	puech
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-24	- coq_makefile: target install now respects the original tree structure	herbelin
2008-12-14	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau
2008-11-23	Minor improvement to commit 11619	herbelin
2008-11-23	Fixed bug #2006 (type constraint on Record was not taken into account) +	herbelin
2008-11-09	More factorization of inductive/record and typeclasses: move class	msozeau
2008-11-05	Move Record desugaring to constrintern and add ability to use notations	msozeau
2008-11-05	Nouvelle syntaxe pour écrire des records (co)inductifs :	aspiwack
2008-10-11	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin
2008-10-03	Minor fixes related to coqdoc and --interpolate and the dependent	msozeau
2008-09-14	Add user syntax for creating hint databases [Create HintDb foo	msozeau
2008-09-14	In manual implicit arguments mode, do not enrich implicits	msozeau
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-28	Fixes in generalize_eqs/dependent induction to allow the user to specify	msozeau
2008-07-24	Suite commit 11236	notin
2008-07-22	Correct implementation of discharging of implicit arguments and add new	msozeau
2008-07-18	Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...	notin
2008-07-18	Affichage intempestif d'information de globalisation + numéro de version dan...	notin
2008-07-17	fixed indentation of subgoals for Show Script	barras
2008-07-17	Uniformisation du format des messages d'erreur (commencent par une	herbelin
2008-07-08	Suite de la révision #11212	notin
2008-07-07	Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...	notin
2008-07-07	- Improve [Context] vernacular to allow arbitrary binders, not just	msozeau
2008-06-29	Lissage de la gestion des chemins de chargement de fichiers :	herbelin
2008-06-25	Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...	notin
2008-06-06	Enhancements to coqdoc, better globalization of sections and modules.	msozeau
2008-06-03	Fix setoid_rewrite documentation examples.	msozeau
2008-05-30	Improvements on coqdoc by adding more information into .glob	msozeau
2008-05-25	- Nouvelle option "Set Printing Existential Instances" pour forcer	herbelin
2008-05-22	Strategy commands are now exported	barras
2008-05-21	refined the conversion oracle	barras
2008-05-12	- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to	msozeau
2008-05-10	Correction bug #1842 + correction bug initialisation introduit dans	herbelin
2008-05-08	Efficacité, bugs, robustesse CoqIDE	herbelin
2008-04-25	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin
2008-04-15	- Add "Global" modifier for instances inside sections with the usual	msozeau
2008-04-12	Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.	msozeau
2008-04-05	- Retour en arrière sur la capacité du nouvel apply à utiliser les	herbelin
2008-04-02	Add the ability to specify the implicit status of section variables and	msozeau
2008-03-23	Fix a bug found by B. Grégoire when declaring morphisms in module	msozeau
2008-03-19	Do another pass on the typeclasses code. Correct globalization of class	msozeau
2008-03-06	Syntax changes in typeclasses, remove "?" for usual implicit arguments	msozeau