aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2018-10-31Merge PR #8825: [libobject] Move object_name next to object definition.Pierre-Marie Pédrot
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[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
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-24Move Heads to pretyping (is_projection will move to Recordops)Gaëtan Gilbert
2018-07-20Also remove ClosedSection (same reasoning as ClosedModule)Maxime Dénès
2018-07-20Remove ClosedModule from libstackMaxime Dénès
2018-07-03Library: use ocaml typing to show that we find at most 2 filesGaëtan Gilbert
2018-07-03Library.register_loaded_library: remove unused variableGaëtan Gilbert
2018-07-03Libobject.apply_dyn_fun: remove unused deflt argumentGaëtan Gilbert
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-19Merge PR #7797: Remove reference name type.Enrico Tassi
2018-06-18Remove reference name type.Maxime Dénès
2018-06-17Getting rid of the const_proj field in the kernel.Pierre-Marie Pédrot
2018-06-14Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ...Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:29:23 +0000