aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/nametab.mli
Commit message (Expand)AuthorAge
* Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Moving the Ltac-specific part of the nametab to the Ltac plugin.Gravatar Pierre-Marie Pédrot2017-10-03
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Adding a trespasser warning to the Nametab API.Gravatar Pierre-Marie Pédrot2017-05-18
* Exporting Nametab generic API.Gravatar Pierre-Marie Pédrot2017-05-03
* Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixing bug #2818.Gravatar Pierre-Marie Pédrot2014-09-03
* Unifying locate code, also making it more powerful: it is now able to findGravatar Pierre-Marie Pédrot2014-07-21
* Adding a new "Locate Term" command, distinct from the raw "Locate" command.Gravatar Pierre-Marie Pédrot2014-07-21
* More complete printing of Ltac location, akin to the term-dedicated Locate co...Gravatar Pierre-Marie Pédrot2014-07-21
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Restrict (try...with...) to avoid catching critical exn (part 6)Gravatar letouzey2013-03-13
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Added command "Locate Ltac qid".Gravatar herbelin2010-06-03
* "make source-doc" builds documentation of mli in html and pdf atGravatar pboutill2010-04-29
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* 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
* Fixed incorrect optimization in Prettyp.pr_located_qualid introducedGravatar herbelin2009-08-07
* Cleaning of Nametab continued + fixed a compilation bug in previous commit.Gravatar herbelin2009-08-06
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Switched to "standardized" names for the properties of eq andGravatar herbelin2009-01-01
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Prise en compte des notations "alias" dans la globalisation des coercions.Gravatar herbelin2007-11-08
* Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)Gravatar herbelin2005-11-21
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Nouvelle en-têteGravatar herbelin2004-07-16
* Nouvelle fonction cherchant tous les noms d'un suffixe donneGravatar herbelin2003-10-21
* Passage des noms de tactiques à kernel_name pour compatibilité avec les fon...Gravatar herbelin2003-06-10
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* *** empty log message ***Gravatar barras2003-03-12
* Pour satisfaire ProofGeneralGravatar coq2003-01-31
* Export M + Module M <: SIGGravatar coq2003-01-09
* Affichage nom le plus court pour Syntactic DefinitionGravatar herbelin2002-11-26
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14