aboutsummaryrefslogtreecommitdiff
path: root/parsing/ppconstr.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-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-09-04Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte lesherbelin
2007-08-30Oubli dans commit 10102...herbelin
2007-08-29- Débogueur: positionnement de set_detype_anonymous pour ne pasherbelin
2007-08-24Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et -recty...herbelin
2007-06-30Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Recordherbelin
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an obl...msozeau
2007-01-10Merge from Lionel Elie Mamane's private branch:lmamane
2006-10-28Ajout option Set Printing Universes et amélioration affichage des universherbelin
2006-10-09Notations:herbelin
2006-09-23Déplacement surround dans util.ml et parenthésage des déclarationsherbelin
2006-07-22- Ajout d'un cast vm dans la syntaxe : x <: t bgregoir
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-30Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...herbelin
2006-05-19Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsortherbelin
2006-04-24Export de pr_lconstr_pattern, pr_lconstr_pattern_env et pr_lpattern_expr;herbelin
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-21Déplacement de pr_arg et pr_opt de Ppconstr vers Utilherbelin
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2005-12-30Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...herbelin
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-12-02Changement des named_contextgregoire
2005-01-02Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...herbelin
2004-12-29ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...herbelin
2004-12-25Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...herbelin
2004-11-04Univ.pr_univ ==> Univ.pr_unisacerdot
2004-11-04Affichage des universherbelin
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-09-09Ajout de or-pattern pour le match-with v8herbelin
2004-08-23Précisions message d'erreurherbelin
2004-07-16Nouvelle en-têteherbelin
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
2003-11-18reparation bug moins unaire (erreur de PP)barras
2003-11-01Extensibilite de la grammaires des patternsherbelin
2003-09-21Mise en place d'implicites par noms en v8herbelin
2003-09-09Ajout construction If primitive dans constr_expr et rawconstrherbelin
2003-09-06Paramétrisation vis à vis de existential_keyherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin