aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/whelp.ml4
Commit message (Expand)AuthorAge
* place all files specific to camlp4 syntax extensions in grammar/Gravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Revert copy/pasted function in to minilib thanks to clib.cmaGravatar pboutill2012-05-23
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
* Noise for nothingGravatar pboutill2012-03-02
* Added a DEPRECATED flag in declaration of options. For now only two options a...Gravatar ppedrot2011-11-24
* Remove dynamic stuff from constr_expr and glob_constrGravatar glondu2011-10-28
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Remove some occurrences of "open Termops"Gravatar glondu2010-09-28
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* 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