aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2018-11-05[Goptions] More detailed error messagesVincent Laporte
2018-11-05Merge PR #8870: Pass native and VM flags to the kernel through environmentPierre-Marie Pédrot
2018-11-05Merge PR #8857: [library] Better sizing for libobject hashtbl.Pierre-Marie Pédrot
2018-11-05Merge PR #8766: [nametab] [api] Provide basic support for efficient completion.Pierre-Marie Pédrot
2018-11-05Pass native and VM flags to the kernel through environmentMaxime Dénès
2018-10-31Use standard combinator for Global.set_strategyMaxime Dénès
2018-10-31Introduce Safe_typing.set_share_reductionMaxime Dénès
2018-10-31Seeing Global purely as a wrapper on top of kernel functions.Hugo Herbelin
2018-10-31[nametab] Move `object_prefix` to `Nametab`.Emilio Jesus Gallego Arias
2018-10-31[nametab] Move global_dir_reference to NametabEmilio Jesus Gallego Arias
2018-10-31Merge PR #8825: [libobject] Move object_name next to object definition.Pierre-Marie Pédrot
2018-10-31[library] Better sizing for libobject hashtbl.Emilio Jesus Gallego Arias
2018-10-29Merge PR #8812: [ssreflect] Better use of CoqlibEnrico Tassi
2018-10-26[libobject] Move object_name next to object definition.Emilio Jesus Gallego Arias
2018-10-26Merge PR #8687: Mini reorganization type of global constr of globalPierre-Marie Pédrot
2018-10-24[Coqlib] Remove redundant checkVincent Laporte
2018-10-19Deprecating Global.type_of_global_in_context.Hugo Herbelin
2018-10-19Deprecating Global.constr_of_global_in_context.Hugo Herbelin
2018-10-19Moving Global.constr_of_global_in_context to Typeops.Hugo Herbelin
2018-10-19Moving Global.type_of_global_in_context to Typeops.Hugo Herbelin
2018-10-18[nametab] [api] Provide basic support for efficient completion.Emilio Jesus Gallego Arias
2018-10-18[api] Qualify access to `Nametab`Emilio Jesus Gallego Arias
2018-10-16Deprecate Global.universes_of_global (replaced by environ version)Gaëtan Gilbert
2018-10-11A state-free version of is_polymorphic.Hugo Herbelin
2018-10-11Adding a functional version of constant_of_delta_kn.Hugo Herbelin
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-08Merge PR #8585: Simplify declaration of universe namesPierre-Marie Pédrot
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-10-04Simplify declaration of universe namesGaëtan Gilbert
2018-10-03Merge PR #8596: [api] Cleanup `Decls`: remove unused function, move vernac he...Pierre-Marie Pédrot
2018-10-01Merge PR #8575: Remove {Safe_typing,Global}.push_contextMaxime Dénès
2018-10-01Merge PR #7634: Extend combined scheme to Schemes in TypeMatthieu Sozeau
2018-09-30[api] Cleanup `Decls`: remove unused function, move vernac helper.Emilio Jesus Gallego Arias
2018-09-27Remove {Safe_typing,Global}.push_contextGaëtan Gilbert
2018-09-27Fix #8478: Undeclared universe anomaly with sectionsGaëtan Gilbert
2018-09-26Combined Scheme tests sort to use either "*" or "/\"Théo Winterhalter
2018-09-23Merge PR #8465: Small cleanup of summary usesPierre-Marie Pédrot
2018-09-20Rewrite "Flags, Options and Tables" section.Jim Fehrle
2018-09-19Replace trivial uses of declare_summary with summary.refsGaëtan Gilbert
2018-09-19Merge PR #8447: Cleaning in the retroknowledgePierre-Marie Pédrot
2018-09-18Removing Dischargedhypsmap which is unused internally.Maxime Dénès
2018-09-14Retroknowledge: use GlobRef.t instead of Constr.t as entryVincent Laporte
2018-09-14Retroknowledge: remove the (unused) by clauseVincent Laporte
2018-09-12Move maps & sets indexed by GlobRef.t into the kernelVincent Laporte
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias
2018-09-03Merge PR #7085: Turn the kernel reduction sharing flag into an argument passe...Maxime Dénès
2018-07-27Merge PR #8164: Add information to option type errorsEnrico Tassi
2018-07-26Merge PR #8101: Remove ClosedModule and ClosedSection from libstackEnrico Tassi
2018-07-26Add information to option type errorsTej Chajed
2018-07-26Turn the kernel reduction sharing flag into an argument passed in the cache.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 17:17:39 +0000