| Commit message (Expand) | Author | Age |
... | |
* | Que le niveau 100 soit associatif à droite dans operconst et à gauche dans ... | herbelin | 2006-07-04 |
* | Extension des motifs disjonctifs au cas de disjonction de motifs multiples | herbelin | 2006-07-03 |
* | Mise à jour (avec retard) des niveaux de la table default_pattern_levels | herbelin | 2006-07-03 |
* | Faire que les niveaux de tactiques soient correctement parsés par ARGUMENT E... | herbelin | 2006-06-23 |
* | Suppresion redondance interp_entry_name entre Q_util et Argextend | herbelin | 2006-06-23 |
* | Added {measure x f} as a valid recursion order. | msozeau | 2006-06-22 |
* | Bug is_number | herbelin | 2006-06-10 |
* | Plus de Declare Module sans vrai type explicite | herbelin | 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-08 |
* | Factorisation utilisation environnement dans make_pr_tac | herbelin | 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 |
* | Changement de précédence de l'argument du by de assert; conséquences... | herbelin | 2006-05-23 |
* | Nouvelle implantation du polymorphisme de sorte pour les familles inductives | herbelin | 2006-05-23 |
* | Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort | herbelin | 2006-05-19 |
* | Oubli des symboles du Latin-1 | herbelin | 2006-05-11 |
* | Centralisation de la détection lettre/symbole par le lexeur dans les plages ... | herbelin | 2006-05-10 |
* | Extension syntaxique de rewrite in: au lieu de pouvoir faire | letouzey | 2006-05-02 |
* | Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '... | notin | 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 |
* | - Utilisation d'abbréviations pour les types intervenant dans RCases | herbelin | 2006-04-26 |
* | Diverses corrections de l'afficheur et du traducteur pour s'assurer de | herbelin | 2006-04-26 |
* | Export de pr_lconstr_pattern, pr_lconstr_pattern_env et pr_lpattern_expr; | herbelin | 2006-04-24 |
* | Si un fixpoint a plusieurs arguments, mais un seul de type inductif, | letouzey | 2006-04-14 |
* | - Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de | herbelin | 2006-03-22 |
* | + destruct now works as induction on multiple arguments : | jforest | 2006-03-21 |
* | Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}. | msozeau | 2006-03-13 |
* | Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf... | herbelin | 2006-03-05 |
* | induction now admits multiple induction arguments. The principle must | coq | 2006-02-10 |
* | Branchement sur nouvelle interface de declare_numeral_interpreter | herbelin | 2006-02-04 |
* | Recherche des global_reference paresseusement pour pouvoir interpréter | herbelin | 2006-02-04 |
* | parsing/g_ascii_syntax.ml | herbelin | 2006-02-04 |
* | Ajout de fichiers d'interprétation de la syntaxe primitive pour string et char | herbelin | 2006-01-31 |
* | Ajout syntaxe concrète Proposition, synonyme de Lemma | herbelin | 2006-01-29 |
* | Réorganisation de la structure interne des types de déclarations (decl_kinds) | herbelin | 2006-01-28 |
* | - Ajout syntaxe concrète Property/Corollary, synonymes de Lemma | herbelin | 2006-01-28 |
* | Correction bug Inspect introduit par le passage du discharge à une méthode ... | herbelin | 2006-01-28 |
* | Ajout option 'using lemmas' à auto/trivial/eauto | herbelin | 2006-01-28 |
* | Suppression code pour hints nommés à la V7 (voire à la V6...) | herbelin | 2006-01-28 |
* | Oubli lors suppression traducteur | herbelin | 2006-01-23 |
* | Messages de idtac et fail peuvent maintenant être des listes de string, int ... | herbelin | 2006-01-21 |
* | Ajout de la contrainte que l'assertion doit être complètement prouvée dans... | herbelin | 2006-01-21 |
* | Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f... | herbelin | 2006-01-21 |
* | Déplacement de pr_arg et pr_opt de Ppconstr vers Util | herbelin | 2006-01-21 |
* | Retrait de 'by' comme mot-clé en espérant qu'il n'y aura pas d'interférenc... | herbelin | 2006-01-18 |
* | Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq | herbelin | 2006-01-16 |
* | - Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses | herbelin | 2006-01-16 |