aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/reduction.ml
Commit message (Expand)AuthorAge
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* improve efficiency of the reduction interpreter of coqtopGravatar Bruno Barras2015-01-06
* Revert commit that inverted the preference for FFlex/FProj problems inGravatar Matthieu Sozeau2014-12-10
* Option -type-in-type continued (deactivate test for inferred sort ofGravatar Hugo Herbelin2014-11-19
* Remove an ununsed pattern and commented code in the kernel.Gravatar Matthieu Sozeau2014-10-24
* Revert "Move eta-expansion after delta reduction in kernel reduction. This ma...Gravatar Matthieu Sozeau2014-10-14
* Move eta-expansion after delta reduction in kernel reduction. This makesGravatar Matthieu Sozeau2014-10-02
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Fix checker to handle projections with eta and universe polymorphism correctly.Gravatar Matthieu Sozeau2014-09-06
* Rename eta_expand_ind_stacks, fix the one from the checker and adaptGravatar Matthieu Sozeau2014-09-05
* Fix infer conv using the wrong universe conversion flexibility informationGravatar Matthieu Sozeau2014-08-03
* Cleanup code for constant equality in kernel conversion.Gravatar Matthieu Sozeau2014-07-21
* Use kernel conversion on terms that contain universe variables during unifica...Gravatar Matthieu Sozeau2014-07-20
* In dest_prod_assum, allow non-toplevel let-reductions (fixes a bug found in M...Gravatar Matthieu Sozeau2014-07-07
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Moving a Thread.yield in check_interrupt.Gravatar Pierre-Marie Pédrot2014-06-07
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
* Make kernel reduction code parametric over the handling of universes,Gravatar Matthieu Sozeau2014-06-06
* - Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed someGravatar Matthieu Sozeau2014-05-28
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* Update infer_conv to record trivial Prop <= Type i constraints that are neede...Gravatar Matthieu Sozeau2014-05-26
* - Fix comparison of universes.Gravatar Matthieu Sozeau2014-05-06
* Restore reasonable performance by not allocating during universe checks,Gravatar Matthieu Sozeau2014-05-06
* Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Paral-ITP: cleanup of command line flags and more conservative defaultGravatar Enrico Tassi2014-01-05
* Support for evars and metas in native compiler.Gravatar Maxime Dénès2013-12-30
* Tentative fix of the guardedness checker by Christine and me. All stdlib and ...Gravatar Matthieu Sozeau2013-12-17
* Reduction: every n iterations a slaves process checks for interruptionGravatar Enrico Tassi2013-11-27
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (kernel)Gravatar ppedrot2012-11-22
* More monomorphizationsGravatar ppedrot2012-11-13
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Univ: enforce_leq instead of enforce_geq for more uniformityGravatar letouzey2012-03-22
* Noise for nothingGravatar pboutill2012-03-02
* Propagated information from the reduction tactics to the kernel soGravatar herbelin2011-08-10
* Esubst: make types of substitutions & lifts privateGravatar puech2011-08-08
* - Remove create_evar_defsGravatar msozeau2011-04-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 16:56:06 +0000