coq - The formal proof system

Age	Commit message (Expand)	Author
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey
2009-02-06	pushed evar reduction in kernel	barras
2008-12-09	About "apply in":	herbelin
2008-08-04	Évolutions diverses et variées.	herbelin
2008-06-10	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin
2008-06-08	- Extension de "generalize" en "generalize c as id at occs".	herbelin
2008-04-13	Bugs, nettoyage, et améliorations diverses	herbelin
2008-04-01	Ajout "simple apply" et "simple eapply" pour apply sans unfold	herbelin
2007-10-03	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2007-04-28	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin
2006-10-28	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin
2006-10-16	affichage des ... dans les scripts	barras
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-05-23	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin
2006-01-11	removes several warnings in contrib/interface	bertot
2005-12-26	Achèvement suppression traducteur dans contrib/interface	herbelin
2005-12-02	Changement des named_context	gregoire
2005-11-02	Types inductifs parametriques	mohring
2004-07-16	Nouvelle en-tête	herbelin
2003-11-25	Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...	herbelin
2003-11-13	factorisation et generalisation des clauses	barras
2003-11-12	Bug TacId	herbelin
2003-10-10	changement nouvelle syntaxe (pt fixes)	barras
2003-06-19	Ajout 'Symmetry in Hyp'	herbelin
2003-03-12	* empty log message *	barras
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-03-27	Simplification de Proof_type.prim_rule	herbelin
2002-02-07	petit nettoyage de kernel/inductive	barras
2001-12-13	compat ocaml 3.03	filliatr
2001-11-12	Suppression des stamps et donc des *_constraints	clrenard
2001-11-06	Suppression des local_constraints, des ctxtty et du focus.	clrenard
2001-11-05	GROS COMMIT:	barras
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-04-19	Making sure there will be no warnings at compile time.	bertot
2001-04-18	Correcting a problem of s that appears behind a Let when there are	bertot
2001-04-18	Adding files for the production of textual explanations as used in pcoq.	bertot