| Age | Commit message (Expand) | Author |
|---|
| 2014-06-29 | When building on-the-fly elimination principles, set the predicates universe ... | Matthieu Sozeau |
| 2014-06-28 | Small short optimization of instantiation in Evd. | Hugo Herbelin |
| 2014-06-20 | Cleanup treatment of template universe polymorphism (thanks to E. Tassi | Matthieu Sozeau |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau |
| 2014-06-18 | Code factorization in LMap. | Pierre-Marie Pédrot |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-13 | Improved error message when a meta posed as an evar remains unsolved | Hugo Herbelin |
| 2014-06-10 | Made explanations for universe inconsistencies optional. They are only used | Pierre-Marie Pédrot |
| 2014-06-10 | - Fix substitution of universes which needlessly hashconsed existing universes. | Matthieu Sozeau |
| 2014-06-10 | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau |
| 2014-06-06 | Make kernel reduction code parametric over the handling of universes, | Matthieu Sozeau |
| 2014-06-04 | - Force every universe level to be >= Prop, so one cannot "go under" it anymore. | Matthieu Sozeau |
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau |
| 2014-06-04 | - Keep all <= constraints during refinement, otherwise we might miss collapse... | 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-08 | - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ... | Matthieu Sozeau |
| 2014-05-06 | - Fix treatment of global universe constraints which should be passed along | Matthieu Sozeau |
| 2014-05-06 | Find a more efficient fix for dealing with template universes: | Matthieu Sozeau |
| 2014-05-06 | Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible. | Matthieu Sozeau |
| 2014-05-06 | - Fix arity handling in retyping (de Bruijn bug!) | Matthieu Sozeau |
| 2014-05-06 | - Fixes for canonical structure resolution (check that the initial term indee... | Matthieu Sozeau |
| 2014-05-06 | - Fix eq_constr_universes restricted to Sorts.equal | Matthieu Sozeau |
| 2014-05-06 | Remove postponed constraints (unused) | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | 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 | - Rename eq to equal in Univ, document new modules, set interfaces. | Matthieu Sozeau |
| 2014-05-06 | Correct rebase on STM code. Thanks to E. Tassi for help on dealing with | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-23 | Better representation of evar filters: we represent the vacuous filters of | Pierre-Marie Pédrot |
| 2014-02-27 | Tacinterp: refactoring using Monad. | Arnaud Spiwack |
| 2014-02-27 | Code refactoring thanks to the new Monad module. | Arnaud Spiwack |
| 2014-01-29 | Using Map.smartmap whenever deemed useful. | Pierre-Marie Pédrot |
| 2013-12-30 | When resetting an evarmap with the unsafe function Evd.evars_reset_evd with | Pierre-Marie Pédrot |
| 2013-11-30 | Useless instantiation function exported in Evd. | Pierre-Marie Pédrot |
| 2013-10-31 | Efficient filtered functions in Evd. We test that a filter is actually | ppedrot |
| 2013-10-30 | Various optimizations of Evd.meta_* functions. | ppedrot |
| 2013-10-30 | More efficient implementation of [Evd.retract_coercible_metas]. | ppedrot |
| 2013-10-29 | Sharing identity evar filters. | ppedrot |
| 2013-10-28 | Removing Evd.undefined_evars. | ppedrot |
| 2013-10-27 | Removing useless filter allocation in evar construction. | ppedrot |
| 2013-10-27 | Abstracting evar filter away. The API is not perfect, but better than nothing. | ppedrot |
| 2013-10-27 | Closure optimizations. | ppedrot |
| 2013-10-23 | cList: set-as-list functions are now with an explicit comparison | letouzey |
| 2013-10-22 | Removing useless array-to-list and converse casts used in | ppedrot |
| 2013-10-22 | Optimizing evar filters. It seems to cost quite a lot in unification, | ppedrot |
| 2013-10-06 | Removing useless evar code. | ppedrot |
| 2013-10-05 | Removing dubious use of evarmap manipulating functions in printing | ppedrot |
| 2013-10-05 | Moving side effects into evar_map. There was no reason to keep another | ppedrot |
