| Commit message (Expand) | Author | Age |
|---|
| * | Add a flush for a warning. |  courtieu | 2006-10-23 |
| * | Notations: |  herbelin | 2006-10-09 |
| * | Annulation de l'essai de changement de sémantique du %scope (révision 9208). | herbelin | 2006-10-06 |
| * | Essai de changement de sémantique du %scope : | herbelin | 2006-10-05 |
| * | 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-24 |
| * | 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-23 |
| * | Protection List.fold_left2 (cf bug #1224) | herbelin | 2006-09-22 |
| * | Declarative Proof Language: main commit |  corbinea | 2006-09-20 |
| * | Export de fonctions d'interprétation acceptant des evars non résolues | herbelin | 2006-09-01 |
| * | Correction bug 1172 + correction en passant de la taille des paramètres de f... | herbelin | 2006-07-07 |
| * | Extension des motifs disjonctifs au cas de disjonction de motifs multiples | herbelin | 2006-07-03 |
| * | documentation | herbelin | 2006-06-23 |
| * | Légère mise à jour | herbelin | 2006-06-22 |
| * | Added {measure x f} as a valid recursion order. |  msozeau | 2006-06-22 |
| * | 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-08 |
| * | Correction trou de subject-reduction de create_arg dans genarg.mli | herbelin | 2006-06-07 |
| * | Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme... | herbelin | 2006-05-30 |
| * | The "clean integration of subtac" patch. | msozeau | 2006-05-29 |
| * | - Déplacement des types paramétriques prod, sum, option, identity, | herbelin | 2006-05-28 |
| * | Adaptation de Coqdoc au nouveau add_glob | notin | 2006-05-24 |
| * | 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-23 |
| * | Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort | herbelin | 2006-05-19 |
| * | 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-28 |
| * | - 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-27 |
| * | - Utilisation d'abbréviations pour les types intervenant dans RCases | herbelin | 2006-04-26 |
| * | Timide tentative de clarification du statut de l'opérateur de filtrage | herbelin | 2006-04-24 |
| * | Si un fixpoint a plusieurs arguments, mais un seul de type inductif, |  letouzey | 2006-04-14 |
| * | - Documentation of the Program tactics. | msozeau | 2006-04-07 |
| * | Amendement impression evar pour affichage des Meta par 'info' | herbelin | 2006-03-31 |
| * | 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-22 |
| * | Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}. | msozeau | 2006-03-13 |
| * | Correction message d'erreur ltac et adoption du modèle de message de Tacinterp | herbelin | 2006-03-04 |
| * | Ajout nat_path et find_reference | herbelin | 2006-02-04 |
| * | Utilisation du section_path pour le parsing des notations primitives, | herbelin | 2006-02-04 |
| * | Adaptation message d'erreur au cas des string | herbelin | 2006-01-31 |
| * | 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-30 |
| * | Bug 'match x in I' (potentiellement utilisable comme cast) | herbelin | 2006-01-29 |
| * | exporting the global reference to the inductive " \/ " in coqlib and |  bertot | 2006-01-25 |
| * | Suppression de la dépendance en Map.fold de ocaml dont la sémantique a | herbelin | 2006-01-24 |
courtieu
herbelin
corbinea
msozeau
notin
letouzey
bertot