aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.ml
AgeCommit message (Expand)Author
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-11-11Addressing #13349: accept Search on subparts of ident, not only on subidents.Hugo Herbelin
2020-10-21Code factorization in Names.Pierre-Marie Pédrot
2020-10-21Similar introduction of a Construct module in the Names API.Pierre-Marie Pédrot
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
2020-10-21Rename the GlobRef comparison modules following the standard pattern.Pierre-Marie Pédrot
2020-10-21Same little game with Projection.Pierre-Marie Pédrot
2020-10-21Deprecate the non-qualified equality functions on kerpairs.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-10-24Raise an anomaly when looking up unknown constant/inductiveGaëtan Gilbert
2019-07-04Merge PR #10359: Remove dependency of native_compile on global env for symbolsMaxime Dénès
2019-06-25Merge PR #10284: Expose set interface to option tablesPierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-12Remove dependency of native_compile on global env for symbolsGaëtan Gilbert
2019-06-03Expose set interface to option tablesGaëtan Gilbert
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-01-06Documenting the internal role of to_string and print in Names.Hugo Herbelin
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-10-20Cleanup comparing projections through their constants.Gaëtan Gilbert
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-24[kernel] Compile with almost all warnings enabled.Emilio Jesus Gallego Arias
2018-09-12Move maps & sets indexed by GlobRef.t into the kernelVincent Laporte
2018-07-24Projections use index representationGaëtan Gilbert
2018-06-18Remove Canary.whitequark
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated aliases from `Names`.Emilio Jesus Gallego Arias
2018-05-30[api] Reintroduce `Names.global_reference` aliasEmilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-21[api] Miscellaneous consolidation + moves to engine.Emilio Jesus Gallego Arias
2017-10-16Use type nonrec in some functor arguments.Gaëtan Gilbert
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-04A few typos.Hugo Herbelin
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-20Revised behavior on ill-formed identifiers.Hugo Herbelin
2017-04-27Remove some unused values and typesGaetan Gilbert
2017-04-20refactoring "Names.DirPath.is_empty" functionMatej Kosik
2017-04-20refactoring "Names.DirPath.compare" functionMatej Kosik
2017-04-20refactoring "Names.DirPath.equal" functionMatej Kosik
2017-04-10Revert "refactoring: Names.DirPath.equal"Matej Košík
2017-04-10Revert "refactoring: Names.DirPath.compare"Matej Košík
2017-04-10Revert "refactoring: Names.DirPath.is_empty"Matej Košík
2017-04-10refactoring: Names.DirPath.is_emptyMatej Kosik
2017-04-10refactoring: Names.DirPath.compareMatej Kosik
2017-04-10refactoring: Names.DirPath.equalMatej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:06:08 +0000