aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.ml
AgeCommit message (Expand)Author
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
2014-12-10Revert commit that inverted the preference for FFlex/FProj problems inMatthieu Sozeau
2014-11-19Option -type-in-type continued (deactivate test for inferred sort ofHugo Herbelin
2014-10-24Remove an ununsed pattern and commented code in the kernel.Matthieu Sozeau
2014-10-14Revert "Move eta-expansion after delta reduction in kernel reduction. This ma...Matthieu Sozeau
2014-10-02Move eta-expansion after delta reduction in kernel reduction. This makesMatthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-09-06Fix checker to handle projections with eta and universe polymorphism correctly.Matthieu Sozeau
2014-09-05Rename eta_expand_ind_stacks, fix the one from the checker and adaptMatthieu Sozeau
2014-08-03Fix infer conv using the wrong universe conversion flexibility informationMatthieu Sozeau
2014-07-21Cleanup code for constant equality in kernel conversion.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:59:03 +0000