aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2018-06-26Merge PR #7919: Fix equality check on global names from native compute.Maxime Dénès
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
2018-06-05Use projection indices in native compilation rather than constant names.Pierre-Marie Pédrot
2018-06-05Merge PR #7643: Fix #7631: native_compute fails to compile an example in Coq 8.8Pierre-Marie Pédrot
2018-06-05Merge PR #7646: Fix #4714: Stack overflow with native computePierre-Marie Pédrot
2018-06-05Merge PR #7495: Fix restrict_universe_contextMatthieu Sozeau
2018-06-04Fix #7631: native_compute fails to compile an example in Coq 8.8Maxime Dénès
2018-06-04Merge PR #7418: Actually take advantage of the normalization status of kernel...Maxime Dénès
2018-06-04Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.Maxime Dénès
2018-06-01Merge PR #7234: Reduce circular dependency constants <-> projectionsMaxime Dénès
2018-05-31Fix #4714: Stack overflow with native computeMaxime Dénès
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated aliases from `Names`.Emilio Jesus Gallego Arias
2018-05-30[api] Reintroduce `Names.global_reference` aliasEmilio Jesus Gallego Arias
2018-05-30Fix restrict_universe_contextGaëtan Gilbert
2018-05-28Fix #7333: vm_compute segfaults / Anomaly with cofixMaxime Dénès
2018-05-28Unify pre_env and envMaxime Dénès
2018-05-28Remove vm_conv hook and reorganize kernel filesMaxime Dénès
2018-05-28Make some comments more precise about compilation of cofixpointsMaxime Dénès
2018-05-28Less confusing debug printing of setfield bytecode instructionMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:31:35 +0000