aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evd.mli
AgeCommit message (Expand)Author
2014-05-06- Fix eq_constr_universes restricted to Sorts.equalMatthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Restore reasonable performance by not allocating during universe checks,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-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-27Tacinterp: refactoring using Monad.Arnaud Spiwack
2014-02-27Code refactoring thanks to the new Monad module.Arnaud Spiwack
2013-11-30Useless instantiation function exported in Evd.Pierre-Marie Pédrot
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-22Removing useless array-to-list and converse casts used inppedrot
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-25Removing useless evar-related stuff.ppedrot
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-05Documentation of Evd.ppedrot
2013-09-03Partly replacing list-based access functions in Evd. This is stillppedrot
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-08-08State Transaction Machinegareuselesinge
2013-08-04Removing now useless merging primitives from Evd.ppedrot
2013-05-06Small cleaning of Evd interface.ppedrot
2013-05-03Removing a redundant function from Evd.ppedrot
2013-04-29Merging Context and Sign.ppedrot
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
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of identifierppedrot
2012-11-22Monomorphization (pretyping)ppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-04-18Adds a comment: precondition on Evd.addaspiwack
2012-03-02Noise for nothingpboutill
2011-12-16Introducing a notion of evar candidates to be used when an evar isherbelin
2011-10-25Continuing r14585 (ill-typed restriction bug).herbelin
2011-06-21Cleaning debugging printer relative to new proof engine. Inherbelin
2011-06-12Added a new flag for freezing evars in tactic unification. Used thisherbelin
2011-05-13A better procedure for checking presence of undefined evars.aspiwack
2011-05-04First phase removing obsolete support for eta up to conversion inherbelin
2011-03-11Tentative to make unification check types at every instanciation of anmsozeau
2011-03-11- Better error messages taking unif. constraints into account.msozeau
2011-03-10Forgot a use of evars_reset_evd in nf_evars, add an optional argument asmsozeau
2011-02-17- Use transparency information all the way through unification andmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 02:21:03 +0000