aboutsummaryrefslogtreecommitdiff
path: root/library/libnames.ml
AgeCommit message (Expand)Author
2014-03-20Missing equalities in Names-like structures.Pierre-Marie Pédrot
2013-12-12Patch for supporting [From Xxx Require Yyy Zzz.]Gregory Malecha
2013-10-23CList.prefix_of and CList.drop_prefix with a parametric equalityletouzey
2013-08-22Nicer code concerning dirpaths and modpath around Libletouzey
2013-04-22Declaremods: some more minor cleanupletouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-11-22Monomorphization (library)ppedrot
2012-11-13More monomorphizationsppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-29Removed many calls to OCaml generic equality. This was done byppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-02Noise for nothingpboutill
2011-10-08Rely on kernel to know if a name is already used so as to be consistent with it.herbelin
2011-05-11Print Module (Type) M now tries to print more detailsletouzey
2011-03-05Added a table for using reserved names for binding names to typesherbelin
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-23First debug... the renaming of librairies was not working and auto/dn were no...soubiran
2009-10-21This big commit addresses two problems:soubiran
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-04-08Some dead code removal + cleanupsletouzey
2009-01-30Correction bug 2037.soubiran
2008-12-24- coq_makefile: target install now respects the original tree structureherbelin
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
2008-06-29Lissage de la gestion des chemins de chargement de fichiers :herbelin
2008-02-22Merge with lmamane's private branch:lmamane
2007-11-09Rétablissement compatibilité constr_of_referenceherbelin
2007-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
2007-01-10Suite commit restructuration discharge (application du type deherbelin
2007-01-10Nouvelle approche pour le discharge modulaireherbelin
2006-04-28 r8931@thot: notin | 2006-04-28 16:19:38 +0200notin
2006-04-27Ajout chop_dirpathherbelin
2005-05-20Adoption du nom canonique global_of_constr pour éviter confusion avec type r...herbelin
2005-02-18Standardisation of constr_of_reference into constr_of_global + Moved Indmap a...herbelin
2005-01-03HUGE COMMITsacerdot
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 04:08:52 +0000