coq - The formal proof system

Age	Commit message (Expand)	Author
2009-12-30	Fixing bug #2146 (broken selection of occurrences in "change").	herbelin
2009-12-21	Generic support for open terms in tactics	herbelin
2009-09-20	Only one "in" clause in "destruct" even for a multiple "destruct".	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-04	- Add more precise error localisation when one of the application fails	herbelin
2009-08-03	Added "etransitivity".	herbelin
2009-08-02	Fixed a typo in "info" for tactic "right".	herbelin
2009-06-06	Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0	herbelin
2009-04-24	Fixing bug #2308 ("instantiate" tactic did not comply with	herbelin
2009-03-16	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin
2008-12-09	About "apply in":	herbelin
2008-10-23	Fix bug #1977 by allowing the [apply] variants to take an [open_constr]	msozeau
2008-09-12	Add a type argument to letin_tac instead of using casts and recomputing	msozeau
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-25	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	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
2008-03-07	f_equal, revert, specialize in ML, contradict in better Ltac (+doc)	letouzey
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