coq - The formal proof system

Age	Commit message (Expand)	Author
2007-01-02	Rework subtac pattern matching equalities generation.	msozeau
2006-12-09	Évitement des noms de constructeurs dans les motifs de filtrage de "match"	herbelin
2006-10-29	Compatibilité du polymorphisme de constantes avec les sections.	herbelin
2006-10-06	Déplacement de on_judgment_type de Typeops vers Termops	herbelin
2006-05-23	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin
2006-02-07	Amélioration des messages d'erreurs de tacred; unfold considère maintenant le	herbelin
2005-05-25	Added subtac contrib.	coq
2005-02-18	Ajout it_mkNamedProd_wo_LetIn	herbelin
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-09-15	hiding the meta_map in evar_defs	barras
2004-09-03	premiere reorganisation de l\'unification	barras
2004-08-24	Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2004-03-15	preparation pour release (suite)	barras
2003-11-24	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin
2003-10-22	Deplacement de iter_constr_with_full_binders dans Termops	herbelin
2003-10-13	Export is_section_variable	herbelin
2003-10-13	Deplacement next_global_ident_away dans Termops	herbelin
2003-09-23	Changement de l'afficheur pour que les variables liées aient un nom indépen...	herbelin
2003-09-13	Deplacement de Declare vers Termops	herbelin
2003-09-12	Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-03-12	* empty log message *	barras
2002-11-18	Allègement du noyau	herbelin
2002-10-09	retour en arriere concernant la recherche d'occurence modulo expansion des le...	barras
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-03-26	Prise en compte des dependances dans la tactique Case	mohring
2002-03-04	Nouveau Rewrite-in plus economique	barras
2002-02-15	petits changements cosmetiques sur les tactiques	barras
2002-02-11	substitution et pattern modulo let	barras
2002-02-07	petit nettoyage de kernel/inductive	barras
2002-01-17	Amélioration affichage échec lookup_eliminator	herbelin
2001-11-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
2001-11-05	GROS COMMIT:	barras