coq - The formal proof system

Age	Commit message (Expand)	Author
2009-03-16	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-09	About "apply in":	herbelin
2008-10-26	Fixes and refinements regarding occurrence selection:	herbelin
2008-08-05	Correction de bugs:	herbelin
2008-08-04	Évolutions diverses et variées.	herbelin
2008-06-16	Add possibility to match on defined hypotheses, using brackets to	msozeau
2008-06-11	Correction de deux bugs liés au commit 11094 sur les clauses "at" et "in".	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-23	Prise en compte des coercions dans les clauses "with" même si le type	herbelin
2008-04-14	Diverses corrections	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
2008-03-07	Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part	msozeau
2008-03-01	Rework on rich forms of rewrite	letouzey
2008-02-01	Unification de TacLetRecIn et TacLetIn. En particulier, on peut	herbelin
2007-10-03	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin
2007-09-30	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin
2007-07-06	Adding a syntax for "n-ary" rewrite:	letouzey
2007-07-06	extension of the rename tactic: the following is now allowed:	letouzey
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2007-04-28	Ajout de la possibilité de faire référence dans certains cas à un nom	herbelin
2007-04-28	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin
2007-04-02	Extension to the general sequence operator (tactical). Now in addition to ...	emakarov
2007-02-01	Suppression de code mort	notin
2006-12-11	Changement dans le kernel :	bgregoir
2006-11-20	Suppression du type 'tac dans les abstract_argument_type: devenu inutile	herbelin
2006-10-24	Extension de la primitive ltac fresh pour qu'elle accepte une liste de	herbelin
2006-06-07	Correction trou de subject-reduction de create_arg dans genarg.mli	herbelin
2006-05-30	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin
2006-05-02	Extension syntaxique de rewrite in: au lieu de pouvoir faire	letouzey
2006-03-21	+ destruct now works as induction on multiple arguments :	jforest
2006-02-10	induction now admits multiple induction arguments. The principle must	coq
2006-01-28	Ajout option 'using lemmas' à auto/trivial/eauto	herbelin
2006-01-21	Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...	herbelin
2006-01-16	Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq	herbelin
2006-01-16	- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-05-17	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin
2005-05-15	Allow auto to have a parametric argument (wish #967)	herbelin
2005-03-07	Added 'clear - id' to clear all hypotheses except the ones dependent in the s...	herbelin
2005-02-04	Ajout constructeur External pour appel outil externe à Coq	herbelin
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-10-11	'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2004-06-29	moved instantiate binding to extratactics	corbinea