aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2018-10-29Merge PR #8780: Cleanup comparing projections through their constants.Maxime Dénès
2018-10-26Merge PR #8684: Remove a few circumvolutions around parameters of inductive e...Gaëtan Gilbert
2018-10-26Merge PR #8687: Mini reorganization type of global constr of globalPierre-Marie Pédrot
2018-10-26Merge PR #8814: Comment Environ.set_universesMaxime Dénès
2018-10-26Remove a few circumvolutions around parameters of inductive entriesMaxime Dénès
2018-10-26Merge PR #8777: Move side-effects into Safe_typingMaxime Dénès
2018-10-26Merge PR #8707: Separate cache representation between CClosure and CBVMaxime Dénès
2018-10-26Merge PR #7186: Moving `fold_constr_with_full_binders` to a placeMaxime Dénès
2018-10-24Comment Environ.set_universesGaëtan Gilbert
2018-10-22Merge PR #8708: Stupid but critical unfolding heuristic.Maxime Dénès
2018-10-20Cleanup comparing projections through their constants.Gaëtan Gilbert
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-19Cleaning layout typeops.mli.Hugo Herbelin
2018-10-19Explicitly merge contexts in side-effect universe handling.Pierre-Marie Pédrot
2018-10-19Move side-effect typing into Safe_env.Pierre-Marie Pédrot
2018-10-16{Univops -> Vars}.universes_of_constrGaëtan Gilbert
2018-10-16UnivGen.extend_context -> Univ.extend_in_context_setGaëtan Gilbert
2018-10-16Simplify vars_of_global usageGaëtan Gilbert
2018-10-16Simplify fresh_foo_instance functions and pretyping of univ instanceGaëtan Gilbert
2018-10-16Deprecate Global.universes_of_global (replaced by environ version)Gaëtan Gilbert
2018-10-16Merge PR #8695: Adding a functional version of constant- and mind_of_delta_kn...Pierre-Marie Pédrot
2018-10-15Correct some spelling errorsBenjamin Barenblat
2018-10-12Moving local copy fold_constr_with_full_binders in assumptions.ml to constr.ml.Hugo Herbelin
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-11Clean up CClosure code.Pierre-Marie Pédrot
2018-10-11The cbv reduction does not rely on the kernel info data structure anymore.Pierre-Marie Pédrot
2018-10-11Stupid but critical unfolding heuristic.Pierre-Marie Pédrot
2018-10-08Merge PR #8654: Remove FCast from CClosure.fterm.Maxime Dénès
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-10-04Remove FCast from CClosure.fterm.Pierre-Marie Pédrot
2018-10-02Merge PR #8572: [config] Miscellaneous cleaning of configuration variables.Pierre-Marie Pédrot
2018-10-02Merge PR #7522: [ocaml] Update required OCaml version to 4.05.0Pierre-Marie Pédrot
2018-10-01Merge PR #8254: Inline the definition of CClosure.mk_clos_deep.Maxime Dénès
2018-10-01Merge PR #8577: Generalize type of compare_head_with functions, and use for e...Pierre-Marie Pédrot
2018-10-01Merge PR #8575: Remove {Safe_typing,Global}.push_contextMaxime Dénès
2018-10-01[nit] Qualify `Envars` use.Emilio Jesus Gallego Arias
2018-09-28Generalize type of compare_head_with functionsGaëtan Gilbert
2018-09-27[dune] [merlin] Fix some usability issues.Emilio Jesus Gallego Arias
2018-09-27Remove {Safe_typing,Global}.push_contextGaëtan Gilbert
2018-09-27Merge PR #8475: Centralize the reliance on abstract universe context internalsGaëtan Gilbert
2018-09-26[ocaml] Update required OCaml version to 4.05.0Emilio Jesus Gallego Arias
2018-09-26Inline the definition of CClosure.mk_clos_deep.Pierre-Marie Pédrot
2018-09-26Merge PR #8534: Checking if low-level name printers are used on purpose or notMaxime Dénès
2018-09-24[kernel] Compile with almost all warnings enabled.Emilio Jesus Gallego Arias
2018-09-23Checking if low-level name printers are used on purpose or not.Hugo Herbelin
2018-09-21Remove hash based univ level compareGaëtan Gilbert
2018-09-21Fix printing of abstract universe contexts.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:17:00 +0000