aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2019-03-22Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ...Maxime Dénès
2019-03-20Merge PR #9776: [kernel] Fix compare_head_gen_leq_with to use [leq] on applic...Gaëtan Gilbert
2019-03-18[kernel] Fix compare_head_gen_leq_with to use [leq] on applicationsMatthieu Sozeau
2019-03-18Remove Term_typing.translate_mind indirectionGaëtan Gilbert
2019-03-18Merge PR #9740: Make NotConvertibleVect exception internal to typeopsPierre-Marie Pédrot
2019-03-14Put [@inline] on CClosure.Mark functionsGaëtan Gilbert
2019-03-14Switch order eqappr/check relevance in conversion.Gaëtan Gilbert
2019-03-14mutable relevance marks in fconstrGaëtan Gilbert
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
2019-03-14Enable proof irrelevance for SProp.Gaëtan Gilbert
2019-03-14Inductives in SProp, forbid primitive records with only sprop fieldsGaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-03-14Make Sorts.t privateGaëtan Gilbert
2019-03-11Make NotConvertibleVect exception internal to typeopsGaëtan Gilbert
2019-03-11Nicer error for bad primitive types (through type_errors etc)Gaëtan Gilbert
2019-03-11Remove unused Retroknowledge.Register_inlineGaëtan Gilbert
2019-03-06Merge PR #9476: Constructor type information uses the expanded form.Gaëtan Gilbert
2019-03-01[Kernel] Simpler generation of opcode filesVincent Laporte
2019-03-01write_uint63.ml: add headerVincent Laporte
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
2019-02-26Fix #9526: Registering inductives for primitive integers doesn't check enoughMaxime Dénès
2019-02-25[kernel] termination checking backtracks on stuck primitive projectionEnrico Tassi
2019-02-25[kernel] termination checking backtracks on stuck fixEnrico Tassi
2019-02-22[kernel] termination checking backtracks on stuck caseEnrico Tassi
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:16:46 +0000