| Commit message (Expand) | Author | Age |
* | Addition of a "Combined Scheme" vernacular command for building the conjuncti... | msozeau | 2006-12-23 |
* | Variable print_instances pour déboguer les instances d'evar | herbelin | 2006-12-12 |
* | Pas d'escamotage des noms réservés si Set Printing All actibvé | herbelin | 2006-12-08 |
* | Remplacement de la dépendance de G_vernac en G_constr (source | herbelin | 2006-12-03 |
* | Suppression du type 'tac dans les abstract_argument_type: devenu inutile | herbelin | 2006-11-20 |
* | 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 |