aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.ml
AgeCommit message (Expand)Author
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
2018-02-11Use specialized function for inductive subtyping inference.Gaëtan Gilbert
2018-02-11dest_{prod,lam}: no Cast case (it's removed by whd)Gaëtan Gilbert
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
2018-02-10[get_cumulativity_constraints] allowing further code sharing.Gaëtan Gilbert
2018-02-10Factorize code for comparing maybe-cumulative inductives.Gaëtan Gilbert
2018-02-07Merge PR #6685: Use whd-all on rigid-flex conversion.Maxime Dénès
2018-02-05Respect the transparent state of the current conversion on strong weak-head.Pierre-Marie Pédrot
2018-02-04Delay computation of lifts in the reduction machine.Pierre-Marie Pédrot
2018-02-02kernel: cleanup projection unfoldingGaëtan Gilbert
2018-02-02Use whd-all on rigid-flex conversion.Pierre-Marie Pédrot
2017-12-14Fixing a bug of Print for inductive types with let-ins in parameters.Hugo Herbelin
2017-12-14Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Maxime Dénès
2017-12-09[api] Remove yet another type alias.Emilio Jesus Gallego Arias
2017-12-09[lib] Rename Profile to CProfileEmilio Jesus Gallego Arias
2017-11-23Make some functions on terms more robust w.r.t new term constructs.Maxime Dénès
2017-11-15Merge PR #6058: Remove redundant env argument to Reduction.ccnvMaxime Dénès
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-11-02Remove redundant env argument to Reduction.ccnvGaëtan Gilbert
2017-07-11Less footguns in universe handling: remove subst_instance_context.Pierre-Marie Pédrot
2017-07-11Getting rid of simple calls to AUContext.instance.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Fix a bug in cumulativityAmin Timany
2017-06-16OptimizationAmin Timany
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-16Fix bugsAmin Timany
2017-06-16Squashed commit of the following:Amin Timany
2017-06-16Fix cum/conv for inductive typesAmin Timany
2017-06-16Use inductive subtyping for conv/cumulAmin Timany
2017-06-14Merge PR#448: Do not recompute twice the whnf of terms in conversion.Maxime Dénès
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-04-27Fix omitted labels in function callsGaetan Gilbert
2017-04-08Fast path in weak head reduction of applied atoms.Pierre-Marie Pédrot
2017-02-27Do not recompute twice the whnf of terms in conversion.Pierre-Marie Pédrot
2017-02-19Optimizing array mapping in the kernel.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:53:23 +0000