aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* New bootstrapping, improved, Makefile systemGravatar corbinea2007-07-13
* More natural notation for intro pattern: @a -> ?aGravatar glondu2007-07-09
* If a fixpoint is not written with an explicit { struct ... }, then Gravatar letouzey2007-07-07
* a few works about my commits since FebruaryGravatar letouzey2007-07-06
* Documentation for commit 9774.Gravatar glondu2007-07-06
* New intro pattern "@A", which generates a fresh name based on A.Gravatar glondu2007-07-06
* - 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 23:21:54 +0000