aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2020-01-27Small API additions to kernel/univGaëtan Gilbert
2020-01-22Fix #11421 computation of Set+2Gaëtan Gilbert
2020-01-21Typo in a comment of univ.mli.Hugo Herbelin
2020-01-15Discharge inductive types without rechecking themGaëtan Gilbert
2020-01-15generate variance data for section universes (not yet used)Gaëtan Gilbert
2020-01-14infercumulativity: take less argumentsGaëtan Gilbert
2020-01-13Native compute: cleanup temporary files on program exitGaëtan Gilbert
2020-01-07cleanup: do not use recargs when computing the reloc table for ctorsGaëtan Gilbert
2020-01-07minor cleanup template_polymorphic_univs: check_levels returns boolGaëtan Gilbert
2020-01-06Fix #11360: discharge of template inductive with param only use of varGaëtan Gilbert
2019-12-27Add critical-bugs entry, tests-suite file, and code comment.Guillaume Melquiond
2019-12-22Use a more straightforward algorithm for mulc on 32-bit architectures. (Fixes...Guillaume Melquiond
2019-12-22Simplify equality of 63-bit integers.Guillaume Melquiond
2019-12-22Do not hide constants from the compiler.Guillaume Melquiond
2019-12-18Merge PR #10616: Fix push_universe_context* interfaces to use a consistent ~s...Pierre-Marie Pédrot
2019-12-18Merge PR #11027: Cleanup post #10647 (expose comind universe handling)Pierre-Marie Pédrot
2019-12-17failwith -> caml_failwithGuillaume Munch-Maccagnoni
2019-12-17Fatal error in VM if SIGINT was seen but no exception occured.Guillaume Munch-Maccagnoni
2019-12-17Fix signal polling for OCaml 4.10Guillaume Munch-Maccagnoni
2019-12-17[VM] fix volatile declarationGuillaume Munch-Maccagnoni
2019-12-16Remove variance info from inductive entries, infer in indtypingGaëtan Gilbert
2019-12-13Use ~strict argument consistently in push_context/push_context_set intfsMatthieu Sozeau
2019-12-12[vm] Untabify the VM C code.Emilio Jesus Gallego Arias
2019-12-07Section.t is never emptyGaëtan Gilbert
2019-12-04[dune] Update to dune language version 2.0Emilio Jesus Gallego Arias
2019-11-26indTyping: error instead of anomaly for ill-formed templateGaëtan Gilbert
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
2019-11-22Use the relevance flag in CClosure rel contexts in an efficient way.Pierre-Marie Pédrot
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-12Merge PR #11092: [dune] Have only one rule calling configureEmilio Jesus Gallego Arias
2019-11-11Have only one dune rule calling configurePierre Roux
2019-11-10Merge PR #10980: Fix #10903: type-in-type allows fixpoints on sprop inductivesPierre-Marie Pédrot
2019-11-08Merge PR #11014: Fix #8459: anomaly not enough abstractions in fix bodyPierre-Marie Pédrot
2019-11-01Communicate CFLAGS to dunePierre Roux
2019-11-01Add a check for gradual underflowsPierre Roux
2019-11-01feat: Use SSE2_MATH if available & Die if missing on x87Erik Martin-Dorel
2019-11-01Fix ldshiftexpPierre Roux
2019-11-01Add "==", "<", "<=" in PrimFloat.vErik Martin-Dorel
2019-11-01Make primitive float work on WindowsPierre Roux
2019-11-01Reimplement is_floatPierre Roux
2019-11-01Make primitive float work on x86_32Pierre Roux
2019-11-01Pretty-printing primitive float constantsErik Martin-Dorel
2019-11-01Add primitive floats to checkerPierre Roux
2019-11-01Add primitive floats to 'native_compute'Pierre Roux
2019-11-01Add next_{up,down} primitive float functionsPierre Roux
2019-11-01Implement classify on primitive floatPierre Roux
2019-11-01Change return type of primitive float comparisonPierre Roux
2019-11-01Put axioms on ldshiftexp and frshiftexpGuillaume Bertholon
2019-11-01Add primitive floats to 'vm_compute'Guillaume Bertholon
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:27:07 +0000