aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* - Ajout de la possibilité d'utiliser la notation Record pour lesGravatar herbelin2007-06-30
* Réaffichage des Structure/Record sous la forme RecordGravatar herbelin2007-05-28
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* Nouveaux changements autour des implicites (notamment suite àGravatar herbelin2007-05-06
* Suite commit 9810Gravatar herbelin2007-04-29
* Ajout de la possibilité de faire référence dans certains cas à un nomGravatar herbelin2007-04-28
* Déplacement des opérations sur bool dans l'état initialGravatar herbelin2007-04-28
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* - Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771Gravatar herbelin2007-04-18
* Added the option to set/unset the automatic generation of elimination schemesGravatar vsiles2007-04-17
* Nettoyage des tactiques basées sur "simpl" (delta-réduction cachantGravatar herbelin2007-04-13
* Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y aGravatar herbelin2007-04-11
* Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5Gravatar herbelin2007-04-10
* Added back the tactics [apply -> ident], etc. to Tactics.v afterGravatar emakarov2007-04-02
* Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGESGravatar herbelin2007-02-21
* Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deGravatar herbelin2007-02-13
* MAJ ringGravatar herbelin2007-01-31
* 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