| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 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 |
