aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2007-05-06Nouveaux changements autour des implicites (notamment suite àherbelin
2007-04-29Suite commit 9810herbelin
2007-04-28Ajout de la possibilité de faire référence dans certains cas à un nomherbelin
2007-04-28Déplacement des opérations sur bool dans l'état initialherbelin
2007-04-28Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.herbelin
2007-04-18- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771herbelin
2007-04-17 Added the option to set/unset the automatic generation of elimination schemesvsiles
2007-04-13Nettoyage des tactiques basées sur "simpl" (delta-réduction cachantherbelin
2007-04-11Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y aherbelin
2007-04-10Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5herbelin
2007-04-02Added back the tactics [apply -> ident], etc. to Tactics.v afteremakarov
2007-02-21Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGESherbelin
2007-02-13Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deherbelin
2007-01-31MAJ ringherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 20:02:00 +0000