aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Suite révision 10495Gravatar herbelin2008-02-01
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* Suite ajout raccourcis à compute et lazy pour réduire tout saufGravatar herbelin2007-11-09
* Cleanup attempt of Hints in *Interface.v files.Gravatar letouzey2007-10-21
* Révision de theories/Logic concernant les axiomes de descriptions.Gravatar herbelin2007-10-03
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* Ajout infos de débogage de "universe inconsistency" quand option SetGravatar herbelin2007-09-30
* Forget to update the CHANGES fileGravatar vsiles2007-09-28
* Reals: prod_f_SO inclut f(0) dans le produit et devient prod_f_R0Gravatar herbelin2007-09-27
* Petit complément au commit 10131.Gravatar herbelin2007-09-21
* Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte lesGravatar herbelin2007-09-04
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 15:04:19 +0000