aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.ml
AgeCommit message (Expand)Author
2017-03-14[safe-string] Enable -safe-string !Emilio Jesus Gallego Arias
2017-03-14[safe_string] library/nameopsEmilio Jesus Gallego Arias
2016-12-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-12-02Fix #5242 - Dubious unsilenceable warning on invalid identifierMaxime Dénès
2016-10-26COMMENT: Names.Cmap and Names.Cmap_envMatej Kosik
2016-08-30CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Matej Kosik
2016-08-24Changing the definition of the "Lib.variable.info" type to enable us to do mo...Matej Kosik
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-03-30Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-22A patch renaming equal into eq in the module dealing withHugo Herbelin
2016-03-22Adding eq/compare/hash for syntactic view atHugo Herbelin
2016-02-18ADD: Names.Name.is_{anonymous,name}Matej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11COMMENTS: added to the "Names.inductive" and "Names.constructor" types.Matej Kosik
2015-12-18COMMENTS: added to the "Names" module.Matej Kosik
2015-09-20Better debug printers for module paths.Maxime Dénès
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02A patch renaming equal into eq in the module dealing withHugo Herbelin
2015-08-02Adding eq/compare/hash for syntactic view atHugo Herbelin
2015-07-30Followup of 9f81b58551.Pierre-Marie Pédrot
2015-07-30Fixing bug #4289 (hash-consing only user part of constant notHugo Herbelin
2015-07-02Display functions for primitive projections.Maxime Dénès
2015-04-16Fixing bug #4190.Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-17Ensuring the good invariants of hashcons table generation in the API.Pierre-Marie Pédrot
2014-12-17Fix (actually, properly implement :) hashconsing of projections,Matthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-20Missing equalities in Names-like structures.Pierre-Marie Pédrot
2014-03-08Using HMaps in global references.Pierre-Marie Pédrot
2014-03-08Also use HMaps in KNmap.Pierre-Marie Pédrot
2014-03-07Using Hashmaps by default in constant and inductive maps. This changes fold andPierre-Marie Pédrot
2014-03-05Canary testing absence of generic equality for KerNamesPierre-Marie Pédrot
2014-03-05Lazily computed hash in KerName.t.Pierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-03Kernel names are implemented using records.Pierre-Marie Pédrot
2014-02-03Allocation-friendly mapping functions in Nametab.Pierre-Marie Pédrot
2013-10-31Fixing Kerpair.hash. Since the beginning, it dit not respect the typeppedrot
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Specializing hash functions for widely used types.ppedrot
2013-10-23cList: a few alternative to hashtbl-based uniquize, distinct, subsetletouzey
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-08-22More complete hashcons : lists (dirpath), arrays (constr)letouzey
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:09:49 +0000