aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* Addition of a "Combined Scheme" vernacular command for building the conjuncti...Gravatar msozeau2006-12-23
* Variable print_instances pour déboguer les instances d'evarGravatar herbelin2006-12-12
* Pas d'escamotage des noms réservés si Set Printing All actibvéGravatar herbelin2006-12-08
* Remplacement de la dépendance de G_vernac en G_constr (sourceGravatar herbelin2006-12-03
* Suppression du type 'tac dans les abstract_argument_type: devenu inutile Gravatar herbelin2006-11-20
* Add a flush for a warning.Gravatar courtieu2006-10-23
* Notations:Gravatar herbelin2006-10-09
* Annulation de l'essai de changement de sémantique du %scope (révision 9208).Gravatar herbelin2006-10-06
* Essai de changement de sémantique du %scope : Gravatar herbelin2006-10-05
* Tentative d'amélioration du message d'erreur en cas de paramètre non laisséGravatar herbelin2006-09-24
* Correction bug dans détection clause "in" mal formée quand le "in" estGravatar herbelin2006-09-24
* Correction bug #1179 (result of Notation.decompose_notation_key in wrong orderGravatar herbelin2006-09-23
* - Correction filtrage des notations impliquant un "match" : la présenceGravatar herbelin2006-09-23
* Protection List.fold_left2 (cf bug #1224)Gravatar herbelin2006-09-22
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Export de fonctions d'interprétation acceptant des evars non résoluesGravatar herbelin2006-09-01
* Correction bug 1172 + correction en passant de la taille des paramètres de f...Gravatar herbelin2006-07-07
* Extension des motifs disjonctifs au cas de disjonction de motifs multiplesGravatar herbelin2006-07-03
* documentationGravatar herbelin2006-06-23
* Légère mise à jourGravatar herbelin2006-06-22
* Added {measure x f} as a valid recursion order.Gravatar msozeau2006-06-22
* Changement du type d'argument 'TacticArgType X' en un typeGravatar herbelin2006-06-08
* Réinitialisation de token_number à chaque compilation d'un nouveau fichier ...Gravatar notin2006-06-08
* Correction trou de subject-reduction de create_arg dans genarg.mliGravatar herbelin2006-06-07
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
* - Déplacement des types paramétriques prod, sum, option, identity,Gravatar herbelin2006-05-28
* Adaptation de Coqdoc au nouveau add_globGravatar notin2006-05-24
* Retour version 8852 de constrintern.mlGravatar herbelin2006-05-23
* Erreur commit constrintern.mlGravatar herbelin2006-05-23
* Changement de précédence de l'argument du by de assert; conséquences...Gravatar herbelin2006-05-23
* Modification de add_glob (support des modules dans Coqdoc)Gravatar notin2006-05-23
* Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsortGravatar herbelin2006-05-19
* r8931@thot: notin | 2006-04-28 16:19:38 +0200Gravatar notin2006-04-28
* Typo dans précédent commit (8755); protection renforcée dans analyse claus...Gravatar herbelin2006-04-28
* - Distinction explicite des parties paramètres et arguments dans le typeGravatar herbelin2006-04-27
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* préparation de add_glob en vue d'isolement de la partie module pourGravatar herbelin2006-04-27
* - Utilisation d'abbréviations pour les types intervenant dans RCasesGravatar herbelin2006-04-26
* Timide tentative de clarification du statut de l'opérateur de filtrageGravatar herbelin2006-04-24
* Si un fixpoint a plusieurs arguments, mais un seul de type inductif, Gravatar letouzey2006-04-14
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
* Amendement impression evar pour affichage des Meta par 'info'Gravatar herbelin2006-03-31
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* - Correction bug calcul mind_consnrealargs, introduit à la révisionGravatar herbelin2006-03-22
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
* Correction message d'erreur ltac et adoption du modèle de message de TacinterpGravatar herbelin2006-03-04
* Ajout nat_path et find_referenceGravatar herbelin2006-02-04
* Utilisation du section_path pour le parsing des notations primitives,Gravatar herbelin2006-02-04
* Adaptation message d'erreur au cas des stringGravatar herbelin2006-01-31