aboutsummaryrefslogtreecommitdiff
path: root/parsing/prettyp.ml
AgeCommit message (Expand)Author
2009-11-11Improving abbreviations/notations + backtrack of semantic change in r12439herbelin
2009-10-28Integrate a few improvements on typeclasses and Program from the equations br...msozeau
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2009-08-07Fixed incorrect optimization in Prettyp.pr_located_qualid introducedherbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-07-15- Granted wish #2138 (support for local binders in syntax of Record fields).herbelin
2009-06-03Ensure the precondition of the partial function [list_chop] holdsmsozeau
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
2008-11-23Fixed bug #2006 (type constraint on Record was not taken into account) +herbelin
2008-09-02Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutherbelin
2008-08-22- New auto hints for transparency/opacity control, not bound to msozeau
2008-07-25Correction d'une incohérence de typage des inductifs polymorphes: lesherbelin
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-05-22Strategy commands are now exportedbarras
2008-05-21refined the conversion oraclebarras
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-15- Add "Global" modifier for instances inside sections with the usualmsozeau
2008-04-12Document the new setoid rewrite tactic, and fix a few things whilemsozeau
2008-03-30Ajout d'abbréviations/notations paramétriquesherbelin
2008-03-19Do another pass on the typeclasses code. Correct globalization of classmsozeau
2008-02-19added products and sorts as possible heads for canonical structurescorbinea
2008-02-14Added default canonical structures (see example in test-suite)corbinea
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-14Correction ordre d'affichage des champs des Recordherbelin
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-05-28Réaffichage des Structure/Record sous la forme Recordherbelin
2007-05-06Nouveaux changements autour des implicites (notamment suite àherbelin
2007-01-10Merge from Lionel Elie Mamane's private branch:lmamane
2006-12-08Suite ajout option -output-contextherbelin
2006-12-08Ajout d'une option -output-context qui affiche le contexte en CCI pur à laherbelin
2006-10-29Compatibilité du polymorphisme de constantes avec les sections.herbelin
2006-10-28Ajout option Set Printing Universes et amélioration affichage des universherbelin
2006-09-23Déplacement surround dans util.ml et parenthésage des déclarationsherbelin
2006-05-23Nouvelle implantation du polymorphisme de sorte pour les familles inductivesherbelin
2006-04-27Standardisation nom option_app en option_mapherbelin
2006-01-28Correction bug Inspect introduit par le passage du discharge à une méthode ...herbelin
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-11-21Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)herbelin
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2005-11-02Types inductifs parametriquesmohring
2005-08-19pas besoin de List.length pour savoir si une liste est videletouzey
2005-02-20Keep ClosedSection marker for resetherbelin
2005-02-18Renaming Print Canonical Structure into Print Canonical Projectionsherbelin