aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2018-11-20Merge PR #7925: Clean transparent stateMaxime Dénès
2018-11-19Merge PR #8894: Print full binders in subtyping incompatible polymorphism error.Pierre-Marie Pédrot
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Proper record type and accessors for transparent states.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-11-19Merge PR #8451: Print Universes SubgraphPierre-Marie Pédrot
2018-11-16Use universe names when printing to dot.Gaëtan Gilbert
2018-11-16Make UGraph printing independent of hash orderGaëtan Gilbert
2018-11-16We improve a little bit in printing universe constraints signature mismatch.Hugo Herbelin
2018-11-16Print full binders in subtyping incompatible polymorphism error.Gaëtan Gilbert
2018-11-15Make set_typing_flags "smart"Gaëtan Gilbert
2018-11-09Use arrays of names instead of lists in abstract universe names.Pierre-Marie Pédrot
2018-11-09Actually store the bound name information in the abstract universe context.Pierre-Marie Pédrot
2018-11-09Force the user to provide names when generating abstract universe contexts.Pierre-Marie Pédrot
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-11-06[checker] Refactor by sharing code with the kernelMaxime Dénès
2018-11-06Move debug term printer to kernelMaxime Dénès
2018-11-05Merge PR #8870: Pass native and VM flags to the kernel through environmentPierre-Marie Pédrot
2018-11-05Merge PR #8866: Check universe instances in TypingPierre-Marie Pédrot
2018-11-05Merge PR #8824: Do not check convertibility of pattern types in the kernelMaxime Dénès
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-31Merge PR #8752: Enable fragile pattern warning in cclosureMaxime Dénès
2018-10-30Remove Environ.set_universes / Typing.enrich_envGaëtan Gilbert
2018-10-30Check univ instances in Typing.Gaëtan Gilbert
2018-10-30Simplify universe handling in environ constant_type functionsGaëtan Gilbert
2018-10-29Do not compare the type arguments in pattern-match branches.Pierre-Marie Pédrot
2018-10-29Do not box fconstr closures in pattern-match branches.Pierre-Marie Pédrot
2018-10-29Integrate convert_shape into convert_stack.Pierre-Marie Pédrot
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-17Enable fragile pattern warning in cclosureGaëtan Gilbert
2018-10-16{Univops -> Vars}.universes_of_constrGaëtan Gilbert
2018-10-16UnivGen.extend_context -> Univ.extend_in_context_setGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:59:45 +0000