aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.ml
AgeCommit message (Expand)Author
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
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-17ALPHA-CONVERSION: in the "Reduction" module: clos_fconv --> clos_gen_convMatej Kosik
2015-12-17ALPHA-CONVERSION: in the "Reduction" module: fconv --> gen_convMatej Kosik
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-12-17CLEANUP: in the Reduction moduleMatej Kosik
2015-12-05Unifying betazeta_applist and prod_applist into a clearer interface.Hugo Herbelin
2015-11-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-22Fixing kernel bug in typing match with let-ins in the arity.Hugo Herbelin
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Conversion of polymorphic inductive types was incomplete in VM and native.Maxime Dénès
2015-10-16Merge branch 'v8.5' into trunkMaxime Dénès
2015-10-16Remove left2right reference from the kernel.Maxime Dénès
2015-10-15Avoid dependency of the pretyper on C code.Maxime Dénès
2015-10-15 Fix #4346 2/2: VM casts were not inferring universe constraints.Maxime Dénès
2015-10-15Fix #4346 1/2: native casts were not inferring universe constraints.Maxime Dénès
2015-10-15Warn user when bytecode compilation fails.Maxime Dénès
2015-10-15Remove now useless exception handler in default conversion.Maxime Dénès
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-14Temporary fix: kernel conversion needs to ignore l2r flag.Maxime Dénès
2015-10-14Remove reference to default conversion function inside the kernel.Maxime Dénès
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-09-14Remove dead code in lazy reduction machine.Maxime Dénès
2015-09-06Output a warning when conversion compilation failed.Maxime Dénès
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2015-01-06improve efficiency of the reduction interpreter of coqtopBruno Barras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:09:33 +0000