aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.ml
AgeCommit message (Expand)Author
2018-02-28Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Maxime Dénès
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
2016-11-30Univs: fix bug #5180Matthieu Sozeau
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-02Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-27Fixing an incompatility introduced in a404360: kernel conversion wasHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 04:14:26 +0000