aboutsummaryrefslogtreecommitdiff
path: root/toplevel/whelp.ml4
AgeCommit message (Expand)Author
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
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-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-08-02Improved parameterization of Coq:herbelin
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
2008-10-23Open notation for declaring record instances.msozeau
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-05-08** Efficacité, bugs, robustesse CoqIDE **herbelin
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
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-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
2007-08-30Mise à jour des paramètres Whelp et ajouts d'options Set Whelp Serverherbelin
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an obl...msozeau
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-12-21Divers; restructuration des points d'entrée de Constrinternherbelin
2005-12-02Changement des named_contextgregoire
2005-05-26No parentheses around f in 'f \subst{...}'herbelin
2005-05-26Utilisation du module Buffer; encodage plus rigoureux des symboles en uriherbelin
2005-05-26Patch to avoid Whelp bug removed.sacerdot
2005-05-20Interface vers outil de recherche Whelpherbelin