aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2007-09-04Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte lesherbelin
2007-07-13New bootstrapping, improved, Makefile systemcorbinea
2007-07-09More natural notation for intro pattern: @a -> ?aglondu
2007-07-07If a fixpoint is not written with an explicit { struct ... }, then letouzey
2007-07-06a few works about my commits since Februaryletouzey
2007-07-06Documentation for commit 9774.glondu
2007-07-06New intro pattern "@A", which generates a fresh name based on A.glondu
2007-06-30- Ajout de la possibilité d'utiliser la notation Record pour lesherbelin
2007-05-28Réaffichage des Structure/Record sous la forme Recordherbelin
2007-05-22Nouvelle stratégie d'unification des types des with-bindings dansherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 04:57:26 +0000