aboutsummaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
AgeCommit message (Expand)Author
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-07-22Constrintern: unified push_name_env and push_loc_name_env; madeherbelin
2010-06-14Added printing of recursive notations in cases pattern (supported by wish 2248).herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-18Fixed some printing bugs.herbelin
2010-04-10Optimized need for delimiters when disjoint scopes for strings andherbelin
2010-01-06Allowed handling of partly-applied record constructors. (Fix for bug #2196.)gmelquio
2009-12-13Deactivating printing of {| |} for records when option Printing All is set.herbelin
2009-11-11Improving abbreviations/notations + backtrack of semantic change in r12439herbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-11-04Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.gmelquio
2009-10-29Revision 12439 continued, printing part (notations to names behaveherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-08Some dead code removal + cleanupsletouzey
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
2009-02-06Fixing #2044 (bad printing of primitive notation at the head ofherbelin
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
2008-10-23Open notation for declaring record instances.msozeau
2008-10-22Affichage des notations récursives:herbelin
2008-10-08Améliorations de l'affichage des coercions suggérées par Georges :herbelin
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
2008-05-06Postpone the search for the recursive argument index from the user givenmsozeau
2008-04-14Diverses corrections herbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
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-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-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-10-05Correction de quelques défauts d'affichage (notations sous "as" pourherbelin
2007-09-21- Fixing bug 1703 ("intros until n" falls back on the variable name whenherbelin
2007-08-29- Débogueur: positionnement de set_detype_anonymous pour ne pasherbelin
2007-06-30Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Recordherbelin
2007-05-10Prise en compte réversibilité des notations de la forme "Notation Nil := @n...herbelin
2007-05-06Nouveaux changements autour des implicites (notamment suite àherbelin
2007-04-29Multiples changements autour des implicites :herbelin
2007-03-20Correction bug affichage des notations des noms de fonctions appliquéesherbelin
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an obl...msozeau
2007-01-22Allègement de l'affichage des références par le printer si possibleherbelin
2007-01-11Ajout d'une option de débogage pour expliciter l'instance des evarsherbelin
2006-12-12Variable print_instances pour déboguer les instances d'evarherbelin
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-07-03Extension des motifs disjonctifs au cas de disjonction de motifs multiplesherbelin