aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2019-04-23Merge PR #9962: [native compiler] Encoding of constructors based on tagsPierre-Marie Pédrot
2019-04-16[doc] [kernel] Add docstrings for native interface functions.Emilio Jesus Gallego Arias
2019-04-16Better error message when OCaml compiler not found for native computeMaxime Dénès
2019-04-15[native compiler] Encoding of constructors based on tagsMaxime Dénès
2019-04-15[native compiler] Remove unused universe argument in LmakeblockMaxime Dénès
2019-04-15[native compiler] Distinguish constant constructors in lambda codeMaxime Dénès
2019-04-14[native compiler] Remove now unused GconstructMaxime Dénès
2019-04-14[native compiler] Remove `Lconstruct` from lambda code.Maxime Dénès
2019-04-05[native compiler] Fix critical bug with primitive projectionsMaxime Dénès
2019-03-31Merge PR #9800: Less conv_tab allocations when pushing relevances, esp skip_p...Pierre-Marie Pédrot
2019-03-28[dune] Don't have `lib` depend on `dynlink`Emilio Jesus Gallego Arias
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-18Less conv_tab allocations when pushing relevances, esp skip_patternGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:22:13 +0000