aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evd.ml
AgeCommit message (Expand)Author
2014-05-06Fix 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.equalMatthieu Sozeau
2014-05-06Remove 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-06Restore 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-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Better representation of evar filters: we represent the vacuous filters ofPierre-Marie Pédrot
2014-02-27Tacinterp: refactoring using Monad.Arnaud Spiwack
2014-02-27Code refactoring thanks to the new Monad module.Arnaud Spiwack
2014-01-29Using Map.smartmap whenever deemed useful.Pierre-Marie Pédrot
2013-12-30When resetting an evarmap with the unsafe function Evd.evars_reset_evd withPierre-Marie Pédrot
2013-11-30Useless instantiation function exported in Evd.Pierre-Marie Pédrot
2013-10-31Efficient filtered functions in Evd. We test that a filter is actuallyppedrot
2013-10-30Various optimizations of Evd.meta_* functions.ppedrot
2013-10-30More efficient implementation of [Evd.retract_coercible_metas].ppedrot
2013-10-29Sharing identity evar filters.ppedrot
2013-10-28Removing Evd.undefined_evars.ppedrot
2013-10-27Removing useless filter allocation in evar construction.ppedrot
2013-10-27Abstracting evar filter away. The API is not perfect, but better than nothing.ppedrot
2013-10-27Closure optimizations.ppedrot
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
2013-10-22Removing useless array-to-list and converse casts used inppedrot
2013-10-22Optimizing evar filters. It seems to cost quite a lot in unification,ppedrot
2013-10-06Removing useless evar code.ppedrot
2013-10-05Removing dubious use of evarmap manipulating functions in printingppedrot
2013-10-05Moving side effects into evar_map. There was no reason to keep anotherppedrot
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-09-05Optimizing some evar_maps manipulation. In particular, using a [map] insteadppedrot
2013-09-05Cleaning up of Evd. Extruding the tower of modules used to define evar_maps.ppedrot
2013-09-03Partly replacing list-based access functions in Evd. This is stillppedrot
2013-08-25Actually using the domain function for maps.ppedrot
2013-08-08State Transaction Machinegareuselesinge
2013-08-04Removing now useless merging primitives from Evd.ppedrot
2013-08-03Small fixes due to the arrival of OCaml 3.12.ppedrot
2013-05-06Small cleaning of Evd interface.ppedrot
2013-05-03Removing a redundant function from Evd.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-12A version of Univ.check_eq with no anomaly for Evd.set_eq_sortletouzey
2013-03-12Allowing different types of, not to be mixed, generic Stores throughppedrot
2013-02-17Locating errors from consider_remaining_unif_problems if possibleherbelin
2013-01-29Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envherbelin
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-18Modulification of nameppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-11-26Removed some FIXME related to equality on universes.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 12:22:58 +0000