| Age | Commit message (Expand) | Author |
| 2006-12-03 | Remplacement de la dépendance de G_vernac en G_constr (source | herbelin |
| 2006-11-20 | Suppression du type 'tac dans les abstract_argument_type: devenu inutile | herbelin |
| 2006-10-23 | Add a flush for a warning. | courtieu |
| 2006-10-09 | Notations: | herbelin |
| 2006-10-06 | Annulation de l'essai de changement de sémantique du %scope (révision 9208). | herbelin |
| 2006-10-05 | Essai de changement de sémantique du %scope : | herbelin |
| 2006-09-24 | Tentative d'amélioration du message d'erreur en cas de paramètre non laissé | herbelin |
| 2006-09-24 | Correction bug dans détection clause "in" mal formée quand le "in" est | herbelin |
| 2006-09-23 | Correction bug #1179 (result of Notation.decompose_notation_key in wrong order | herbelin |
| 2006-09-23 | - Correction filtrage des notations impliquant un "match" : la présence | herbelin |
| 2006-09-22 | Protection List.fold_left2 (cf bug #1224) | herbelin |
| 2006-09-20 | Declarative Proof Language: main commit | corbinea |
| 2006-09-01 | Export de fonctions d'interprétation acceptant des evars non résolues | herbelin |
| 2006-07-07 | Correction bug 1172 + correction en passant de la taille des paramètres de f... | herbelin |
| 2006-07-03 | Extension des motifs disjonctifs au cas de disjonction de motifs multiples | herbelin |
| 2006-06-23 | documentation | herbelin |
| 2006-06-22 | Légère mise à jour | herbelin |
| 2006-06-22 | Added {measure x f} as a valid recursion order. | msozeau |
| 2006-06-08 | Changement du type d'argument 'TacticArgType X' en un type | herbelin |
| 2006-06-08 | Réinitialisation de token_number à chaque compilation d'un nouveau fichier ... | notin |
| 2006-06-07 | Correction trou de subject-reduction de create_arg dans genarg.mli | herbelin |
| 2006-05-30 | Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme... | herbelin |
| 2006-05-29 | The "clean integration of subtac" patch. | msozeau |
| 2006-05-28 | - Déplacement des types paramétriques prod, sum, option, identity, | herbelin |
| 2006-05-24 | Adaptation de Coqdoc au nouveau add_glob | notin |
| 2006-05-23 | Retour version 8852 de constrintern.ml | herbelin |
| 2006-05-23 | Erreur commit constrintern.ml | herbelin |
| 2006-05-23 | Changement de précédence de l'argument du by de assert; conséquences... | herbelin |
| 2006-05-23 | Modification de add_glob (support des modules dans Coqdoc) | notin |
| 2006-05-19 | Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort | herbelin |
| 2006-04-28 | r8931@thot: notin | 2006-04-28 16:19:38 +0200 | notin |
| 2006-04-28 | Typo dans précédent commit (8755); protection renforcée dans analyse claus... | herbelin |
| 2006-04-27 | - Distinction explicite des parties paramètres et arguments dans le type | herbelin |
| 2006-04-27 | Standardisation nom option_app en option_map | herbelin |
| 2006-04-27 | préparation de add_glob en vue d'isolement de la partie module pour | herbelin |
| 2006-04-26 | - Utilisation d'abbréviations pour les types intervenant dans RCases | herbelin |
| 2006-04-24 | Timide tentative de clarification du statut de l'opérateur de filtrage | herbelin |
| 2006-04-14 | Si un fixpoint a plusieurs arguments, mais un seul de type inductif, | letouzey |
| 2006-04-07 | - Documentation of the Program tactics. | msozeau |
| 2006-03-31 | Amendement impression evar pour affichage des Meta par 'info' | herbelin |
| 2006-03-22 | Made pretyping a functor over a coercion implementation. Pretyping.Default us... | msozeau |
| 2006-03-22 | - Correction bug calcul mind_consnrealargs, introduit à la révision | herbelin |
| 2006-03-13 | Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}. | msozeau |
| 2006-03-04 | Correction message d'erreur ltac et adoption du modèle de message de Tacinterp | herbelin |
| 2006-02-04 | Ajout nat_path et find_reference | herbelin |
| 2006-02-04 | Utilisation du section_path pour le parsing des notations primitives, | herbelin |
| 2006-01-31 | Adaptation message d'erreur au cas des string | herbelin |
| 2006-01-30 | Déplacement du test du bon nombre d'argument des constructeurs (et de | herbelin |
| 2006-01-30 | Nettoyage warning (dont flush et affichage seulement si mode verbose) | herbelin |
| 2006-01-29 | Bug 'match x in I' (potentiellement utilisable comme cast) | herbelin |