aboutsummaryrefslogtreecommitdiff
path: root/interp/topconstr.ml
AgeCommit message (Expand)Author
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-07-07Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...notin
2008-07-04Fixes in handling of implicit arguments:msozeau
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
2008-05-24Ajout de la possibilité d'utiliser fix/cofix dans les notations.herbelin
2008-05-10- Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desherbelin
2008-05-06Postpone the search for the recursive argument index from the user givenmsozeau
2008-03-30Ajout d'abbréviations/notations paramétriquesherbelin
2008-03-28- Second pass on implementation of let pattern. Parse "let ' par [as x]?msozeau
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
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