aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2018-07-14[ltac] Remove unused functions / constructors.Emilio Jesus Gallego Arias
2018-07-03Term_typing: remove unused argument to internal function.Gaëtan Gilbert
2018-07-03Cooking.cook_constant: remove unused env argument.Gaëtan Gilbert
2018-07-03Indtypes: remove unused is_unit.Gaëtan Gilbert
2018-07-03Subtyping.check_constant: remove unused module path argument.Gaëtan Gilbert
2018-07-03Inductive.extract_stack,filter_stack_domain: remove unused argumentsGaëtan Gilbert
2018-07-03Nativecode compile_mind, compile_mind_field: remove unused argumentsGaëtan Gilbert
2018-07-03Nativecode.pp_mllam internal pp_letrec: remove unused argument.Gaëtan Gilbert
2018-07-03Modops.add_retroknowledge: remove unused argument.Gaëtan Gilbert
2018-06-29Merge PR #7080: Swapping Context and Constr and defining declarations on cons...Maxime Dénès
2018-06-28Deprecate Environ.retroknowledge function in favor of the projectionGaëtan Gilbert
2018-06-28[env.env_rel_context.env_rel_ctx] -> [rel_context env]Gaëtan Gilbert
2018-06-28Make Environ.globals abstract.Gaëtan Gilbert
2018-06-27Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)Pierre-Marie Pédrot
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-27Merge PR #7863: Remove Sorts.contentsPierre-Marie Pédrot
2018-06-27Test file for #7723Maxime Dénès
2018-06-27Fix #7723: vm_compute segfaults with universe polymorphismMaxime Dénès
2018-06-26Merge PR #7919: Fix equality check on global names from native compute.Maxime Dénès
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-25Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...Matthieu Sozeau
2018-06-25Fix equality check on global names from native compute.Pierre-Marie Pédrot
2018-06-24Merge PR #7772: [native_compute] Delay computations with toplevel matchPierre-Marie Pédrot
2018-06-23Merge PR #7614: Simplify the code that handles trust of side-effects in kerne...Maxime Dénès
2018-06-23Adapt the kernel to generate proper data for mutual records.Pierre-Marie Pédrot
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-06-23Change the proj_ind field from MutInd.t to inductive.Pierre-Marie Pédrot
2018-06-23Merge PR #7715: Simplify the cooking of primitive projections.Maxime Dénès
2018-06-22Merge PR #7600: Faster and cleaner fconstr-to-constr conversion function.Maxime Dénès
2018-06-22Remove hack skipping comparison of algebraic universes in subtyping.Gaëtan Gilbert
2018-06-22Define and use UGraph.enforce_leq_alg for subtyping inferenceGaëtan Gilbert
2018-06-19Fix Univ.enforce_leq dropped constraints when algebraic on the rightGaëtan Gilbert
2018-06-19Merge PR #7841: Remove CanaryPierre-Marie Pédrot
2018-06-18Remove Canary.whitequark
2018-06-17Remove the proj_body field from the kernel.Pierre-Marie Pédrot
2018-06-17Remove the proj_eta field of the kernel.Pierre-Marie Pédrot
2018-06-17Remove special declaration of primitive projections in the kernel.Pierre-Marie Pédrot
2018-06-17Getting rid of the const_proj field in the kernel.Pierre-Marie Pédrot
2018-06-17Faster and cleaner fconstr-to-constr conversion function.Pierre-Marie Pédrot
2018-06-17Merge PR #7635: Define rec_declaration in terms of prec_declaration.Maxime Dénès
2018-06-17Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.Maxime Dénès
2018-06-13Merge PR #7677: [api] Remove MisctypesPierre-Marie Pédrot
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-06-12[VM] Rename reloc -> cenvMaxime Dénès
2018-06-11Simplify the cooking of primitive projections.Pierre-Marie Pédrot
2018-06-11[native_compute] Delay computations with toplevel matchMaxime Dénès
2018-06-10[VM] Remove projection names from structured constants.Maxime Dénès
2018-06-07Fix #7615: Functor inlining drops universe substitution.Pierre-Marie Pédrot
2018-06-05Define rec_declaration in terms of prec_declaration.SimonBoulier
2018-06-05More straightforward native compilation of primitive projections.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:40:19 +0000