aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Nouvelle approche pour le discharge modulaireGravatar herbelin2007-01-10
* gestion speciale du niveau 5 des ltacGravatar barras2006-11-02
* fixed field_simplify + changed precedence of let and fun in ltacGravatar barras2006-10-30
* MAJGravatar herbelin2006-10-28
* MAJGravatar herbelin2006-10-06
* avertissement a propos du commit 9211 dans CHANGESGravatar letouzey2006-10-05
* Correction bug #1204 + maj CHANGESGravatar notin2006-10-04
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* Ajout d'une valeur VList dans tacinterp pour permettre de cabler desGravatar herbelin2006-09-22
* MAJGravatar herbelin2006-09-15
* MAJGravatar herbelin2006-09-01
* Diverses modifications autour de l'unification modulo conversion:Gravatar herbelin2006-08-28
* MAJ doc/refmanGravatar notin2006-07-11
* MAJGravatar herbelin2006-07-11
* MAJGravatar herbelin2006-07-07
* MAJGravatar herbelin2006-07-06
* MAJ docGravatar herbelin2006-07-05
* MAJ du manuel de référenceGravatar notin2006-07-04
* MAJGravatar herbelin2006-06-15
* MAJGravatar herbelin2006-06-14
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8948 85f007b7-540e-04...Gravatar jforest2006-06-12
* Nouvelle MAJGravatar herbelin2006-06-09
* changements de dernieres minutes pour la 8.1 beta: Gravatar letouzey2006-06-09
* nouvelle MAJGravatar herbelin2006-06-08
* replace byGravatar herbelin2006-06-07
* Ajout WhelpGravatar herbelin2006-06-07
* MAJGravatar herbelin2006-05-23
* ajout de mes modifs recentesGravatar letouzey2006-05-18
* Centralisation de la détection lettre/symbole par le lexeur dans les plages ...Gravatar herbelin2006-05-10
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
* ajout d'entrées dans TODO et CHANGES (à re-mettre à jour avant la release)Gravatar courtieu2006-04-11
* MAJGravatar herbelin2006-03-05
* Ajout 'exists! x:A, PGravatar herbelin2006-02-23
* Nettoyage Zmin.v, création Zmax.v et Zminmax.vGravatar herbelin2006-02-12
* Ajout bibliothèque String de Laurent ThéryGravatar herbelin2006-02-08
* Idem numbering of 'Unfold', 'simpl', ...Gravatar herbelin2006-02-07
* Mise en conformité de l'ordre des occurrences de pattern avec l'affichageGravatar herbelin2006-02-07
* MAJGravatar herbelin2006-02-07
* coq_makefileGravatar herbelin2006-02-06
* MAJ (synonymes de Lemma; auto using)Gravatar herbelin2006-01-29
* Export eassumptionGravatar herbelin2006-01-19
* Extended Unicode supportGravatar herbelin2006-01-19
* Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nomGravatar herbelin2006-01-16
* - Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesGravatar herbelin2006-01-16
* Ajout paramétricité du nom de la base de hint dans auto et trivialGravatar herbelin2006-01-11
* MAJGravatar herbelin2006-01-07
* Suppression des parseurs et printeurs v7; suppression du traducteur; changeme...Gravatar herbelin2005-12-26
* *** empty log message ***Gravatar herbelin2005-12-23
* MAJGravatar herbelin2005-12-21
* Declare Implicit TacticGravatar herbelin2005-09-09