aboutsummaryrefslogtreecommitdiff
path: root/library/nametab.mli
AgeCommit message (Expand)Author
2018-06-18Remove reference name type.Maxime Dénès
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-10-03Moving the Ltac-specific part of the nametab to the Ltac plugin.Pierre-Marie Pédrot
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-05-18Adding a trespasser warning to the Nametab API.Pierre-Marie Pédrot
2017-05-03Exporting Nametab generic API.Pierre-Marie Pédrot
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-09-03Fixing bug #2818.Pierre-Marie Pédrot
2014-07-21Unifying locate code, also making it more powerful: it is now able to findPierre-Marie Pédrot
2014-07-21Adding a new "Locate Term" command, distinct from the raw "Locate" command.Pierre-Marie Pédrot
2014-07-21More complete printing of Ltac location, akin to the term-dedicated Locate co...Pierre-Marie Pédrot
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 6)letouzey
2013-02-19Dir_path --> DirPathletouzey
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-02Noise for nothingpboutill
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-06-03Added command "Locate Ltac qid".herbelin
2010-04-29"make source-doc" builds documentation of mli in html and pdf atpboutill
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
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-07Fixed incorrect optimization in Prettyp.pr_located_qualid introducedherbelin
2009-08-06Cleaning of Nametab continued + fixed a compilation bug in previous commit.herbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-01-01Switched to "standardized" names for the properties of eq andherbelin
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
2007-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
2005-11-21Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)herbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2004-07-16Nouvelle en-têteherbelin
2003-10-21Nouvelle fonction cherchant tous les noms d'un suffixe donneherbelin
2003-06-10Passage des noms de tactiques à kernel_name pour compatibilité avec les fon...herbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-03-12*** empty log message ***barras
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 14:40:03 +0000