| Age | Commit message (Expand) | Author |
|---|
| 2014-10-02 | Move eta-expansion after delta reduction in kernel reduction. This makes | Matthieu Sozeau |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-09-13 | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin |
| 2014-09-06 | Fix checker to handle projections with eta and universe polymorphism correctly. | Matthieu Sozeau |
| 2014-09-05 | Rename eta_expand_ind_stacks, fix the one from the checker and adapt | Matthieu Sozeau |
| 2014-08-03 | Fix infer conv using the wrong universe conversion flexibility information | Matthieu Sozeau |
| 2014-07-21 | Cleanup code for constant equality in kernel conversion. | Matthieu Sozeau |
| 2014-07-20 | Use kernel conversion on terms that contain universe variables during unifica... | Matthieu Sozeau |
| 2014-07-07 | In dest_prod_assum, allow non-toplevel let-reductions (fixes a bug found in M... | Matthieu Sozeau |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-10 | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau |
| 2014-06-07 | Moving a Thread.yield in check_interrupt. | Pierre-Marie Pédrot |
| 2014-06-07 | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot |
| 2014-06-06 | Make kernel reduction code parametric over the handling of universes, | Matthieu Sozeau |
| 2014-05-28 | - Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed some | Matthieu Sozeau |
| 2014-05-26 | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau |
| 2014-05-26 | Update 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-06 | Restore reasonable performance by not allocating during universe checks, | Matthieu Sozeau |
| 2014-05-06 | Properly reinstate old-style polymorphism in the kernel and pretyping/retyping. | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-01-05 | Paral-ITP: cleanup of command line flags and more conservative default | Enrico Tassi |
| 2013-12-30 | Support for evars and metas in native compiler. | Maxime Dénès |
| 2013-12-17 | Tentative fix of the guardedness checker by Christine and me. All stdlib and ... | Matthieu Sozeau |
| 2013-11-27 | Reduction: every n iterations a slaves process checks for interruption | Enrico Tassi |
| 2013-10-31 | Conv_orable made functional and part of pre_env | gareuselesinge |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-22 | Monomorphization (kernel) | ppedrot |
| 2012-11-13 | More monomorphizations | ppedrot |
| 2012-11-08 | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-03-22 | Univ: enforce_leq instead of enforce_geq for more uniformity | letouzey |
| 2012-03-02 | Noise for nothing | pboutill |
| 2011-08-10 | Propagated information from the reduction tactics to the kernel so | herbelin |
| 2011-08-08 | Esubst: make types of substitutions & lifts private | puech |
| 2011-04-13 | - Remove create_evar_defs | msozeau |
| 2011-03-05 | Starting being more explicit on the reasons why module subtyping fails. | herbelin |
| 2010-12-18 | Univ.constraints made fully abstract instead of being a Set of abstract stuff | letouzey |
| 2010-10-04 | Forgotten lifts in eta-expansion | glondu |
| 2010-09-23 | Fix inconsistency in Prop/Set conversion check | glondu |
| 2010-09-20 | Added eta-expansion in kernel, type inference and tactic unification, | herbelin |
| 2010-07-29 | kernel conversion and reduction do not raise assert failure on ill-typed term... | barras |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-03 | "Improved" the form of the inferred type of "match" by | herbelin |
