coq - The formal proof system

Age	Commit message (Expand)	Author
2005-02-18	Moving centralised discharge into dispatched discharge_function; required to ...	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2004-01-02	meilleure presentation des commentaires du traducteur	barras
2003-09-06	Mise en place possibilité de définitions locales dans les paramètres des r...	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-06-03	Intgration uniforme de coercions dans les dclarations (Variable and co) et re...	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-05-13	Utilisation des de Bruijn pour la constructions des records et de leur projec...	herbelin
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-03-15	entetes	filliatr
2001-02-14	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin
2001-01-24	Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...	herbelin
2001-01-24	Ajout de constantes locales dans les Records	herbelin
2000-12-19	Découpage des différentes fonctionnalités de build_mutual et definition_st...	herbelin
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-01-11	Ajout de Record	herbelin
1999-12-03	- global_reference traite des variables	filliatr
1999-12-02	Version initiale	herbelin