aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
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-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
2018-06-12[api] Remove Misctypes.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: remove dummy alias.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: module_kind to DeclaremodsEmilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: multi to tactics/rewriteEmilio Jesus Gallego Arias
2018-06-01Merge PR #7234: Reduce circular dependency constants <-> projectionsMaxime Dénès
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
2018-05-30[api] Remove deprecated objects in engine / interp / libraryEmilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-05-18Merge PR #6965: [api] Move universe syntax to `Glob_term`Pierre-Marie Pédrot
2018-05-11Merge PR #7340: Remove DirClosedSection.Enrico Tassi
2018-05-11Merge PR #7341: Don't recurse into closed modules/sections in split_lib.Enrico Tassi
2018-05-08[api] Move universe syntax to `Glob_term`Emilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-24Don't recurse into closed modules/sections in split_lib.Jasper Hugunin
2018-04-24Remove DirClosedSection.Jasper Hugunin