aboutsummaryrefslogtreecommitdiff
path: root/interp/topconstr.ml
AgeCommit message (Expand)Author
2008-01-17Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...msozeau
2008-01-15Generalize instance declarations to any context, better name handling. Add ho...msozeau
2008-01-05Correction bug #1749 (datant de l'implantation des or-patterns) +herbelin
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-06Commit intermédiaire express de réparation de coqide.ml, que j'avais aspiwack
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-08-29- Débogueur: positionnement de set_detype_anonymous pour ne pasherbelin
2007-05-29Correction d'un bug dans l'affichage du message d'erreur real_cleanherbelin
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an obl...msozeau
2006-12-03Remplacement de la dépendance de G_vernac en G_constr (sourceherbelin
2006-10-09Notations:herbelin
2006-10-06Annulation de l'essai de changement de sémantique du %scope (révision 9208).herbelin
2006-10-05Essai de changement de sémantique du %scope : herbelin
2006-09-23- Correction filtrage des notations impliquant un "match" : la présenceherbelin
2006-09-22Protection List.fold_left2 (cf bug #1224)herbelin
2006-07-07Correction bug 1172 + correction en passant de la taille des paramètres de f...herbelin
2006-07-03Extension des motifs disjonctifs au cas de disjonction de motifs multiplesherbelin
2006-06-22Added {measure x f} as a valid recursion order.msozeau
2006-05-29The "clean integration of subtac" patch.msozeau
2006-04-27- Distinction explicite des parties paramètres et arguments dans le typeherbelin
2006-04-27Standardisation nom option_app en option_mapherbelin
2006-04-14Si un fixpoint a plusieurs arguments, mais un seul de type inductif, letouzey
2006-03-13Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.msozeau
2006-01-29Bug 'match x in I' (potentiellement utilisable comme cast)herbelin
2006-01-11Résidus du traducteur v7 -> v8herbelin
2006-01-11Résidus du traducteur v7 -> v8herbelin
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2006-01-09Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement...herbelin
2006-01-08Prise en compte, enfin, du contexte des types de retour de ACases et RCasesherbelin
2006-01-08Ajout rawconstr_of_aconstrherbelin
2005-12-30Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-12-02Changement des named_contextgregoire
2005-06-03Prise en compte de l'utilisation des notations récursives pour faire une not...herbelin
2005-01-13Construct "T with (Definition|Module) id := c" generalized tosacerdot
2005-01-03HUGE COMMITsacerdot
2004-12-25Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...herbelin
2004-11-17Suppression capture des variables par lieurs non liés dans Notation; simplif...herbelin
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-09-15hiding the meta_map in evar_defsbarras
2004-09-09Ajout de or-pattern pour le match-with v8herbelin
2004-08-23Interpretation et affichage corrects des notations LetTuple, affichage des no...herbelin
2004-07-16Nouvelle en-têteherbelin
2004-06-27Typo (bug #797)herbelin
2004-04-08Chgt role 2eme argument AList et implantation affichage motifs recursifs de n...herbelin
2004-03-19Bug protection array_fold_left2herbelin
2004-03-17Motifs recursifs de notations: prise en compte de l'associativite et des nota...herbelin
2004-03-17Mise en place de motifs récursifs dans Notation; quelques simplifications au...herbelin
2004-03-05modif des fixpoints pour que si on donne une notation au produit, les pts fix...barras
2004-02-26Keep structure information for Fixpoint declaration and Fix termsbertot