| Age | Commit message (Expand) | Author |
|---|
| 2007-10-03 | Révision de theories/Logic concernant les axiomes de descriptions. | herbelin |
| 2007-10-03 | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin |
| 2007-09-30 | Ajout infos de débogage de "universe inconsistency" quand option Set | herbelin |
| 2007-09-28 | Forget to update the CHANGES file | vsiles |
| 2007-09-27 | Reals: prod_f_SO inclut f(0) dans le produit et devient prod_f_R0 | herbelin |
| 2007-09-21 | Petit complément au commit 10131. | herbelin |
| 2007-09-04 | Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte les | herbelin |
| 2007-07-13 | New bootstrapping, improved, Makefile system | corbinea |
| 2007-07-09 | More natural notation for intro pattern: @a -> ?a | glondu |
| 2007-07-07 | If a fixpoint is not written with an explicit { struct ... }, then | letouzey |
| 2007-07-06 | a few works about my commits since February | letouzey |
| 2007-07-06 | Documentation for commit 9774. | glondu |
| 2007-07-06 | New 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 les | herbelin |
| 2007-05-28 | Réaffichage des Structure/Record sous la forme Record | herbelin |
| 2007-05-22 | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin |
| 2007-05-06 | Nouveaux changements autour des implicites (notamment suite à | herbelin |
| 2007-04-29 | Suite commit 9810 | herbelin |
| 2007-04-28 | Ajout de la possibilité de faire référence dans certains cas à un nom | herbelin |
| 2007-04-28 | Déplacement des opérations sur bool dans l'état initial | herbelin |
| 2007-04-28 | Ajout 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 9771 | herbelin |
| 2007-04-17 | Added the option to set/unset the automatic generation of elimination schemes | vsiles |
| 2007-04-13 | Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant | herbelin |
| 2007-04-11 | Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y a | herbelin |
| 2007-04-10 | Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5 | herbelin |
| 2007-04-02 | Added back the tactics [apply -> ident], etc. to Tactics.v after | emakarov |
| 2007-02-21 | Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES | herbelin |
| 2007-02-13 | Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de | herbelin |
| 2007-01-31 | MAJ ring | herbelin |
| 2007-01-10 | Nouvelle approche pour le discharge modulaire | herbelin |
| 2006-11-02 | gestion speciale du niveau 5 des ltac | barras |
| 2006-10-30 | fixed field_simplify + changed precedence of let and fun in ltac | barras |
| 2006-10-28 | MAJ | herbelin |
| 2006-10-06 | MAJ | herbelin |
| 2006-10-05 | avertissement a propos du commit 9211 dans CHANGES | letouzey |
| 2006-10-04 | Correction bug #1204 + maj CHANGES | notin |
| 2006-09-26 | mise a jour du nouveau ring et ajout du nouveau field, avant renommages | barras |
| 2006-09-22 | Ajout d'une valeur VList dans tacinterp pour permettre de cabler des | herbelin |
| 2006-09-15 | MAJ | herbelin |
| 2006-09-01 | MAJ | herbelin |
| 2006-08-28 | Diverses modifications autour de l'unification modulo conversion: | herbelin |
| 2006-07-11 | MAJ doc/refman | notin |
| 2006-07-11 | MAJ | herbelin |
| 2006-07-07 | MAJ | herbelin |
| 2006-07-06 | MAJ | herbelin |
| 2006-07-05 | MAJ doc | herbelin |
| 2006-07-04 | MAJ du manuel de référence | notin |
| 2006-06-15 | MAJ | herbelin |
| 2006-06-14 | MAJ | herbelin |
