aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.ml
AgeCommit message (Expand)Author
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
2010-09-23Fix inconsistency in Prop/Set conversion checkglondu
2010-09-20Added eta-expansion in kernel, type inference and tactic unification,herbelin
2010-07-29kernel conversion and reduction do not raise assert failure on ill-typed term...barras
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-03"Improved" the form of the inferred type of "match" byherbelin
2010-05-09Added a few informations about file lineages (for the most part in kernel)herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-11Ensures that let-in's in arities of inductive types work well. Maybe notherbelin
2009-02-06pushed evar reduction in kernelbarras
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:09:00 +0000