aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.ml
AgeCommit message (Expand)Author
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
2014-07-20Use kernel conversion on terms that contain universe variables during unifica...Matthieu Sozeau
2014-07-07In dest_prod_assum, allow non-toplevel let-reductions (fixes a bug found in M...Matthieu Sozeau
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-06-10Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Matthieu Sozeau
2014-06-07Moving a Thread.yield in check_interrupt.Pierre-Marie Pédrot
2014-06-07Adding a new Control file centralizing the control options of Coq.Pierre-Marie Pédrot
2014-06-06Make kernel reduction code parametric over the handling of universes,Matthieu Sozeau
2014-05-28- Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed someMatthieu Sozeau
2014-05-26- Fix in kernel conversion not folding the universe constraintsMatthieu Sozeau
2014-05-26Update infer_conv to record trivial Prop <= Type i constraints that are neede...Matthieu Sozeau
2014-05-06- Fix comparison of universes.Matthieu Sozeau
2014-05-06Restore reasonable performance by not allocating during universe checks,Matthieu Sozeau
2014-05-06Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-01-05Paral-ITP: cleanup of command line flags and more conservative defaultEnrico Tassi
2013-12-30Support for evars and metas in native compiler.Maxime Dénès
2013-12-17Tentative fix of the guardedness checker by Christine and me. All stdlib and ...Matthieu Sozeau
2013-11-27Reduction: every n iterations a slaves process checks for interruptionEnrico Tassi
2013-10-31Conv_orable made functional and part of pre_envgareuselesinge
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-14Modulification of identifierppedrot
2012-11-22Monomorphization (kernel)ppedrot
2012-11-13More monomorphizationsppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-03-22Univ: enforce_leq instead of enforce_geq for more uniformityletouzey
2012-03-02Noise for nothingpboutill
2011-08-10Propagated information from the reduction tactics to the kernel soherbelin
2011-08-08Esubst: make types of substitutions & lifts privatepuech
2011-04-13- Remove create_evar_defsmsozeau
2011-03-05Starting being more explicit on the reasons why module subtyping fails.herbelin
2010-12-18Univ.constraints made fully abstract instead of being a Set of abstract stuffletouzey
2010-10-04Forgotten lifts in eta-expansionglondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 10:04:59 +0000