aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/whelp.ml4
Commit message (Expand)AuthorAge
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* ** Efficacité, bugs, robustesse CoqIDE **Gravatar herbelin2008-05-08
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Prise en compte des notations "alias" dans la globalisation des coercions.Gravatar herbelin2007-11-08
* Mise à jour des paramètres Whelp et ajouts d'options Set Whelp ServerGravatar herbelin2007-08-30
* Add a parameter to QuestionMark evar kind to say it can be turned into an obl...Gravatar msozeau2007-03-19
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Divers; restructuration des points d'entrée de ConstrinternGravatar herbelin2005-12-21
* Changement des named_contextGravatar gregoire2005-12-02
* No parentheses around f in 'f \subst{...}'Gravatar herbelin2005-05-26
* Utilisation du module Buffer; encodage plus rigoureux des symboles en uriGravatar herbelin2005-05-26
* Patch to avoid Whelp bug removed.Gravatar sacerdot2005-05-26
* Interface vers outil de recherche WhelpGravatar herbelin2005-05-20