aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/nameops.ml
Commit message (Expand)AuthorAge
* [safe_string] library/nameopsGravatar Emilio Jesus Gallego Arias2017-03-14
* COMMENT: was added to "Nameops.increment_suffix".Gravatar Matej Kosik2016-10-19
* CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Gravatar Matej Kosik2016-10-19
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
|/
* Fixing anomaly #3743 while printing an error message involving evar constraints.Gravatar Hugo Herbelin2015-07-16
* Update headers.Gravatar Maxime Dénès2015-01-12
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Less "Coq" strings everywhereGravatar letouzey2013-08-22
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Minor code cleanups, especially take advantage of Dir_path.is_emptyGravatar letouzey2013-02-18
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (library)Gravatar ppedrot2012-11-22
* More monomorphizationsGravatar ppedrot2012-11-13
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Noise for nothingGravatar pboutill2012-03-02
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fix premature optimisation in dependent induction: even variable args needGravatar msozeau2009-04-10
* Correction bug #1041 (double cause : non évitement des noms existants enGravatar herbelin2006-12-12
* Ajout combinateurs option_fold_left et name_fold_mapGravatar herbelin2006-10-09
* Changement anomaly en failwith dans out_name pour utilisation par map_succeedGravatar herbelin2006-04-24
* Prise en compte dans cut_ident des idents de la form _23 qui sont officiellem...Gravatar herbelin2004-10-12
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* Nouvelle en-têteGravatar herbelin2004-07-16
* name_app accessible a tous dans NameopsGravatar herbelin2003-12-19
* Fonctions utilesGravatar herbelin2003-09-23
* errorGravatar herbelin2003-09-09
* Déplacement traducteur de nom dans Constrextern pour accès aux noms longsGravatar herbelin2003-06-10
* Extension renommageGravatar herbelin2003-05-20
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Deplacement lemmes sur fact de Reals vers ArithGravatar herbelin2003-05-14
* Orthographe anglaise - typosGravatar herbelin2003-05-13
* Orthographe anglaiseGravatar herbelin2003-05-13
* En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...Gravatar herbelin2003-04-29
* Renommage unicite/unicity pour la v8Gravatar herbelin2003-04-07
* Mise en place d'un traducteur de noms v7->v8Gravatar herbelin2003-03-31
* Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)Gravatar herbelin2003-03-29
* Petit netoyage dans libGravatar coq2002-12-19
* Corrections de gestion des univers et modules + meilleure gestions des noms...Gravatar coq2002-12-09
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02