aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.ml
AgeCommit message (Expand)Author
2020-03-31Merge PR #11684: Remove spurious anomalies in kernel reductionPierre-Marie Pédrot
2020-03-19Remove spurious anomalies in kernel reductionGaëtan Gilbert
2020-03-18Rename Retypeops -> RelevanceopsGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
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-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-03-18Less conv_tab allocations when pushing relevances, esp skip_patternGaëtan Gilbert
2019-03-18Merge PR #9740: Make NotConvertibleVect exception internal to typeopsPierre-Marie Pédrot
2019-03-14Switch order eqappr/check relevance in conversion.Gaëtan Gilbert
2019-03-14Enable proof irrelevance for SProp.Gaë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-11Make NotConvertibleVect exception internal to typeopsGaëtan Gilbert
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-11-20Use a closure for the domain argument of FProd.Pierre-Marie Pédrot
2018-11-20Do not wrap FProd return types in a closure.Pierre-Marie Pédrot
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-10-29Do not compare the type arguments in pattern-match branches.Pierre-Marie Pédrot
2018-10-29Do not box fconstr closures in pattern-match branches.Pierre-Marie Pédrot
2018-10-29Integrate convert_shape into convert_stack.Pierre-Marie Pédrot
2018-10-11The cbv reduction does not rely on the kernel info data structure anymore.Pierre-Marie Pédrot
2018-10-04Remove FCast from CClosure.fterm.Pierre-Marie Pédrot
2018-09-24[kernel] Compile with almost all warnings enabled.Emilio Jesus Gallego Arias
2018-07-24Projections use index representationGaëtan Gilbert
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-22Define and use UGraph.enforce_leq_alg for subtyping inferenceGaëtan Gilbert
2018-06-04Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.Maxime Dénès
2018-05-28Fix #7333: vm_compute segfaults / Anomaly with cofixMaxime Dénès
2018-05-28Remove vm_conv hook and reorganize kernel filesMaxime Dénès
2018-05-23Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.Hugo Herbelin
2018-05-13Fix #4403: insufficient handling of type-in-type in kernel.Gaëtan Gilbert
2018-03-09Fix expected number of arguments for cumulative constructors.Gaëtan Gilbert
2018-03-09Merge PR #6775: Allow using cumulativity without forcing strict constraints.Maxime Dénès
2018-03-09Merge PR #6769: Split closure cache and remove whd_bothMaxime Dénès
2018-03-09Cumulativity: improve treatment of irrelevant universes.Gaëtan Gilbert
2018-03-08Relax conversion of constructors according to the pCuIC modelMatthieu Sozeau
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04Remove whd_both from the kernel.Pierre-Marie Pédrot
2018-03-04Pass the constant cache as a separate argument in kernel reduction.Pierre-Marie Pédrot
2018-02-28Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-12Merge PR #1082: Fixing Print for inductive types with let-in in parametersMaxime Dénès
2018-02-12Merge PR #6128: Simplification: cumulativity information is variance informa...Maxime Dénès
2018-02-12Merge PR #6674: Delay computation of lifts in the reduction machine.Maxime Dénès
2018-02-11Universe instance printer: add optional variance argument.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:44:57 +0000