aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evd.ml
Commit message (Expand)AuthorAge
* Bettre pretty-printing of evar maps, avoids printing universe informationGravatar Matthieu Sozeau2014-08-13
* Using the asymmetric merging primitive in Evd.Gravatar Pierre-Marie Pédrot2014-08-09
* Cleaning up interface of ContextSet.Gravatar Pierre-Marie Pédrot2014-08-09
* Tentative performance fix for Evd.merge_uctx.Gravatar Pierre-Marie Pédrot2014-08-09
* Small code simplification.Gravatar Pierre-Marie Pédrot2014-08-05
* Use kernel conversion on terms that contain universe variables during unifica...Gravatar Matthieu Sozeau2014-07-20
* When defining a monomorphic Program, do not allow arbitrary instantiationsGravatar Matthieu Sozeau2014-07-03
* Clarifying 'No such bound variable' message in apply, as suggested in #2387Gravatar Hugo Herbelin2014-06-30
* When building on-the-fly elimination principles, set the predicates universe ...Gravatar Matthieu Sozeau2014-06-29
* Small short optimization of instantiation in Evd.Gravatar Hugo Herbelin2014-06-28
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Code factorization in LMap.Gravatar Pierre-Marie Pédrot2014-06-18
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Improved error message when a meta posed as an evar remains unsolvedGravatar Hugo Herbelin2014-06-13
* Made explanations for universe inconsistencies optional. They are only usedGravatar Pierre-Marie Pédrot2014-06-10
* - Fix substitution of universes which needlessly hashconsed existing universes.Gravatar Matthieu Sozeau2014-06-10
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Make kernel reduction code parametric over the handling of universes,Gravatar Matthieu Sozeau2014-06-06
* - Force every universe level to be >= Prop, so one cannot "go under" it anymore.Gravatar Matthieu Sozeau2014-06-04
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* - Keep all <= constraints during refinement, otherwise we might miss collapse...Gravatar Matthieu Sozeau2014-06-04
* - Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed someGravatar Matthieu Sozeau2014-05-28
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...Gravatar Matthieu Sozeau2014-05-08
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
* Find a more efficient fix for dealing with template universes:Gravatar Matthieu Sozeau2014-05-06
* Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible.Gravatar Matthieu Sozeau2014-05-06
* - Fix arity handling in retyping (de Bruijn bug!)Gravatar Matthieu Sozeau2014-05-06
* - Fixes for canonical structure resolution (check that the initial term indee...Gravatar Matthieu Sozeau2014-05-06
* - Fix eq_constr_universes restricted to Sorts.equalGravatar Matthieu Sozeau2014-05-06
* Remove postponed constraints (unused)Gravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* - Fix comparison of universes.Gravatar Matthieu Sozeau2014-05-06
* Restore reasonable performance by not allocating during universe checks,Gravatar Matthieu Sozeau2014-05-06
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Better representation of evar filters: we represent the vacuous filters ofGravatar Pierre-Marie Pédrot2014-04-23
* Tacinterp: refactoring using Monad.Gravatar Arnaud Spiwack2014-02-27
* Code refactoring thanks to the new Monad module.Gravatar Arnaud Spiwack2014-02-27
* Using Map.smartmap whenever deemed useful.Gravatar Pierre-Marie Pédrot2014-01-29
* When resetting an evarmap with the unsafe function Evd.evars_reset_evd withGravatar Pierre-Marie Pédrot2013-12-30
* Useless instantiation function exported in Evd.Gravatar Pierre-Marie Pédrot2013-11-30
* Efficient filtered functions in Evd. We test that a filter is actuallyGravatar ppedrot2013-10-31
* Various optimizations of Evd.meta_* functions.Gravatar ppedrot2013-10-30
* More efficient implementation of [Evd.retract_coercible_metas].Gravatar ppedrot2013-10-30
* Sharing identity evar filters.Gravatar ppedrot2013-10-29
* Removing Evd.undefined_evars.Gravatar ppedrot2013-10-28
* Removing useless filter allocation in evar construction.Gravatar ppedrot2013-10-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 15:13:52 +0000