coq - The formal proof system

Age	Commit message (Expand)	Author
2007-12-05	Factorisation des opérations sur le type option de Util dans un module	aspiwack
2007-10-03	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin
2007-07-06	extension of the rename tactic: the following is now allowed:	letouzey
2007-05-22	Nouvelle stratégie d'unification des types des with-bindings dans	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-12-11	Changement dans le kernel :	bgregoir
2006-05-30	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin
2006-04-27	Standardisation nom option_app en option_map	herbelin
2006-01-16	- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses	herbelin
2005-03-07	Added 'clear - id' to clear all hypotheses except the ones dependent in the s...	herbelin
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-07-16	Nouvelle en-tête	herbelin
2004-06-28	more evar stuff	corbinea
2004-06-26	effective evar refining	corbinea
2004-03-01	Déplacement définition intro_pattern_expr dans Genarg	herbelin
2004-01-09	bugs avec Pose et Assert	barras
2003-11-13	factorisation et generalisation des clauses	barras
2003-11-06	Added Instantiate ... in	corbinea
2003-10-10	changement nouvelle syntaxe (pt fixes)	barras
2003-06-19	Ajout 'Symmetry in Hyp'	herbelin
2003-06-13	Utilisation de intro_pattern dans NewDestruct/NewInduction	herbelin
2003-05-21	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2003-03-12	* empty log message *	barras
2003-01-25	Un type "standardisé" pour new_hyp	herbelin
2002-12-09	Ajout Simpl et Change sur des sous-termes	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-10-21	Ajout d'un suffixe "as [ names ]" pour nommer manuellement les	herbelin
2002-10-21	NewDestruct/NewInduction acceptent l'option "using"	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2001-06-25	Les réduction dans les hypothèses s'appliquent maintenant au corps de la d�...	herbelin
2001-03-15	entetes	filliatr
2000-05-03	Ajout du langage de tactiques	delahaye
1999-11-24	Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations	filliatr
1999-11-23	modules Indrec, Tacentries, Hiddentac	filliatr