aboutsummaryrefslogtreecommitdiff
path: root/parsing/ppvernac.ml
AgeCommit message (Expand)Author
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-11-09Nettoyage de Print Assumptions :aspiwack
2007-09-28Modification of the Scheme command.vsiles
2007-08-24Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et -recty...herbelin
2007-05-30Corrections dans le Print Assumption. Les definitions locales ("Let") aspiwack
2007-05-25Modification of VernacScheme to handle a new scheme: Equality (equality invsiles
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
2007-05-06Nouveaux changements autour des implicites (notamment suite àherbelin
2007-04-29Ajout possibilité d'options à trois mots.herbelin
2007-04-28Ajout de la possibilité de faire référence dans certains cas à un nomherbelin
2007-04-25New keyword "Inline" for Parameters and Axioms for automatic soubiran
2007-02-24Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)herbelin
2007-01-31Fix order of wf and measure arguments, patch Program doc.msozeau
2007-01-11Petit oubli dans commit 9474herbelin
2007-01-10Nouvelle approche pour le discharge modulaireherbelin
2006-12-23Addition of a "Combined Scheme" vernacular command for building the conjuncti...msozeau
2006-09-20Declarative Proof Language: main commitcorbinea
2006-09-01Ajout possibilité clause "where" dans co-points fixes herbelin
2006-08-22making otags working jforest
2006-07-05Branchement de 'Debug On/Off' sur le mécanisme standard d'option et donc, re...herbelin
2006-06-22Added {measure x f} as a valid recursion order.msozeau
2006-05-19Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsortherbelin
2006-04-26Diverses corrections de l'afficheur et du traducteur pour s'assurer deherbelin
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-28Réorganisation de la structure interne des types de déclarations (decl_kinds)herbelin
2006-01-28Suppression code pour hints nommés à la V7 (voire à la V6...)herbelin
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2005-12-28Remplacement Pp.qs par Pptactic.qsnewherbelin
2005-12-27Autres suppressions de composantes du traducteurherbelin
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin