| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2006-01-25 | exporting the global reference to the inductive " \/ " in coqlib and | bertot |
| 2006-01-24 | Suppression de la dépendance en Map.fold de ocaml dont la sémantique a | herbelin |
| 2006-01-16 | Version préliminaire d'inversion de la compilation du filtrage | herbelin |
| 2006-01-16 | Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nom | herbelin |
| 2006-01-11 | Résidus du traducteur v7 -> v8 | herbelin |
| 2006-01-11 | Résidus du traducteur v7 -> v8 | herbelin |
| 2006-01-11 | Restructuration et simplification des fonctions d'affichage, de détypage | herbelin |
| 2006-01-09 | Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement... | herbelin |
| 2006-01-08 | Prise en compte, enfin, du contexte des types de retour de ACases et RCases | herbelin |
| 2006-01-08 | Prise en compte de notations numérales définies au niveau utilisateur + tra... | herbelin |
| 2006-01-08 | Enregistrement dans glob.dump des utilisations de notations numériques (qui ... | herbelin |
| 2006-01-08 | Automatisation de l'utilisation de token primitifs dans les motifs de filtrag... | herbelin |
| 2006-01-08 | Ajout rawconstr_of_aconstr | herbelin |
| 2006-01-05 | Suite révision 1.100 et synthèse optimale des 2 approches possibles: si la ... | herbelin |
| 2006-01-04 | Suppression des coercions non seulement avant l'affichage des notations mais ... | herbelin |
| 2006-01-03 | Redéclaration de la notation à l'import pour être cohérent avec l'activat... | herbelin |
| 2005-12-30 | Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de... | herbelin |
| 2005-12-30 | Ajout booléens; nettoyage | herbelin |
| 2005-12-26 | Petite correction nom QuantHypArgType suite suppression traducteur | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin |
| 2005-12-23 | Simplifification de vernac_expr li l'abandon du traducteur | herbelin |
