aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2007-01-10Nouvelle approche pour le discharge modulaireherbelin
2006-11-02gestion speciale du niveau 5 des ltacbarras
2006-10-30fixed field_simplify + changed precedence of let and fun in ltacbarras
2006-10-28MAJherbelin
2006-10-06MAJherbelin
2006-10-05avertissement a propos du commit 9211 dans CHANGESletouzey
2006-10-04Correction bug #1204 + maj CHANGESnotin
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
2006-09-22Ajout d'une valeur VList dans tacinterp pour permettre de cabler desherbelin
2006-09-15MAJherbelin
2006-09-01MAJherbelin
2006-08-28Diverses modifications autour de l'unification modulo conversion:herbelin
2006-07-11MAJ doc/refmannotin
2006-07-11MAJherbelin
2006-07-07MAJherbelin
2006-07-06MAJherbelin
2006-07-05MAJ docherbelin
2006-07-04MAJ du manuel de référencenotin
2006-06-15MAJherbelin
2006-06-14MAJherbelin
2006-06-12git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8948 85f007b7-540e-04...jforest
2006-06-09Nouvelle MAJherbelin
2006-06-09changements de dernieres minutes pour la 8.1 beta: letouzey
2006-06-08nouvelle MAJherbelin
2006-06-07replace byherbelin
2006-06-07Ajout Whelpherbelin
2006-05-23MAJherbelin
2006-05-18ajout de mes modifs recentesletouzey
2006-05-10Centralisation de la détection lettre/symbole par le lexeur dans les plages ...herbelin
2006-04-28Standardisation du nom des méthodes de Evdherbelin
2006-04-11ajout d'entrées dans TODO et CHANGES (à re-mettre à jour avant la release)courtieu
2006-03-05MAJherbelin
2006-02-23Ajout 'exists! x:A, Pherbelin
2006-02-12Nettoyage Zmin.v, création Zmax.v et Zminmax.vherbelin
2006-02-08Ajout bibliothèque String de Laurent Théryherbelin
2006-02-07Idem numbering of 'Unfold', 'simpl', ...herbelin
2006-02-07Mise en conformité de l'ordre des occurrences de pattern avec l'affichageherbelin
2006-02-07MAJherbelin
2006-02-06coq_makefileherbelin
2006-01-29MAJ (synonymes de Lemma; auto using)herbelin
2006-01-19Export eassumptionherbelin
2006-01-19Extended Unicode supportherbelin
2006-01-16Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nomherbelin
2006-01-16- Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesherbelin
2006-01-11Ajout paramétricité du nom de la base de hint dans auto et trivialherbelin
2006-01-07MAJherbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur; changeme...herbelin
2005-12-23*** empty log message ***herbelin
2005-12-21MAJherbelin
2005-09-09Declare Implicit Tacticherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 20:28:26 +0000