aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2019-02-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
2019-02-08Remove global output_native_objects flag.Gaëtan Gilbert
2019-02-05Merge PR #9373: Kernel: don't automatically downgrade ill-shaped primitive re...Pierre-Marie Pédrot
2019-02-05Merge PR #9438: Cleanup universe length for inductives in vconvPierre-Marie Pédrot
2019-02-04[dune] Fix Dune build in Windows.Emilio Jesus Gallego Arias
2019-02-04Merge PR #6914: Primitive integersPierre-Marie Pédrot
2019-02-04Primitive integersMaxime Dénès
2019-01-30Cleanup universe length for inductives in vconvGaëtan Gilbert
2019-01-30Restrict universes in records.Gaëtan Gilbert
2019-01-24Kernel: don't automatically downgrade ill-shaped primitive recordsGaëtan Gilbert
2019-01-21Refactor typechecking of inductive typesGaëtan Gilbert
2019-01-21Move inductive typecheck to file independent from positivity check.Gaëtan Gilbert
2019-01-21Move inductive_error to Type_errorsGaëtan Gilbert
2019-01-06Documenting the internal role of to_string and print in Names.Hugo Herbelin
2018-12-23Remove dead code from CClosure.Pierre-Marie Pédrot
2018-12-19Merge PR #9159: Make ugraph implementation abstract wrt universe specificsPierre-Marie Pédrot
2018-12-17Make ugraph implementation abstract wrt universe specificsGaëtan Gilbert
2018-12-14[dune] [gitlab] Test OCaml trunk.Emilio Jesus Gallego Arias
2018-12-12checker: check inductive types by roundtrip through the kernel.Gaëtan Gilbert
2018-12-12Merge PR #8974: Fix mod_subst wrt universe polymorphismMaxime Dénès
2018-12-12Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comme...Maxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-12-06Revise API for global universes.Gaëtan Gilbert
2018-12-06Fix race condition triggered by fresh universe generationMaxime Dénès
2018-12-05Fix mod_subst wrt universe polymorphismGaëtan Gilbert
2018-11-30Merge PR #9068: [dune] Minor tweak of dependencies.Théo Zimmermann
2018-11-27Fix #8364: making univ algebraic when already equal to another.Gaëtan Gilbert
2018-11-27Merge PR #8850: Private universes for opaque polymorphic constants.Matthieu Sozeau
2018-11-27Merge PR #8255: Fast typing of application nodesMaxime Dénès
2018-11-26[dune] Minor tweak of dependencies.Emilio Jesus Gallego Arias
2018-11-26Put -indices-matter in typing_flagsGaëtan Gilbert
2018-11-24Merge PR #8929: Fix fixpoint related lifting in open recursors + related clea...Pierre-Marie Pédrot
2018-11-23Merge PR #8995: Don't redeclare constraints of fields in IncludeMaxime Dénès
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-20Add a check that the return stack of an FProd is indeed empty.Pierre-Marie Pédrot
2018-11-20Use a closure for the domain argument of FProd.Pierre-Marie Pédrot
2018-11-20More efficient implementation of type_of_apply.Pierre-Marie Pédrot
2018-11-20Do not wrap FProd return types in a closure.Pierre-Marie Pédrot
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-16Don't redeclare constraints of fields in IncludeGaëtan Gilbert
2018-11-16Fix lifting in foo_with_full_binders for (co)fixpointsGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:50:24 +0000