aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarsolve.ml
AgeCommit message (Expand)Author
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
2020-04-09Code simplification in find_projectable_vars.Pierre-Marie Pédrot
2020-04-09Remove a unused computation in alias code.Pierre-Marie Pédrot
2020-04-09Inline an alias-computing function only used once.Pierre-Marie Pédrot
2020-04-09Remove dead code in Evarsolve alias resolution.Pierre-Marie Pédrot
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-08Ensure that template parameters are shared in the same inductive block.Pierre-Marie Pédrot
2020-02-03Do not return a full term in Evarsolve alias expansion.Pierre-Marie Pédrot
2020-02-03Delay lifting in Evarsolve aliasing.Pierre-Marie Pédrot
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2019-05-23Fixing typos - Part 3JPR
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-04-10Remove calls to Global.env from EvarsolveMaxime Dénès
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-08evarsolve transp_state and comments fixesMatthieu Sozeau
2019-02-08[evarconv] Handle frozen evars in solve_unif_constraints_with_heuristicsMatthieu Sozeau
2019-02-08Add an helper [instantiate_evar] functionMatthieu Sozeau
2019-02-08Flags of evar_conv_x/unifiers: rationalizeMatthieu Sozeau
2019-02-08Rename types_or_terms and the unification function typesMatthieu Sozeau
2019-02-08[evarconv] New flag handling for unifierMatthieu Sozeau
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-12Fix #8908: incorrect refresh of algebraic universes.Gaëtan Gilbert
2018-10-31Renaming is_template_polymorphic -> is_template_polymorphic_ind.Hugo Herbelin
2018-10-29Fix for bug #8848Matthieu Sozeau
2018-10-26[typeclasses] functionalize typeclass evar handlingMatthieu Sozeau
2018-10-26Cleanup evar_extra: remove evar_info's store and add maps to evar_mapMatthieu Sozeau
2018-10-16Simplify vars_of_global usageGaëtan Gilbert
2018-10-14Removing a call to Global.env in evarsolve.Hugo Herbelin
2018-10-08Fix #5197, handling of algebraic universesMatthieu Sozeau
2018-10-07[api] Deprecate `evar_map` ref combinators.Emilio Jesus Gallego Arias
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-09-14Fixing yet a source of dependency on alphabetic order in unification.Hugo Herbelin
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-12Fixes #7780 (missing lift in expanding alias under a binder in unification).Hugo Herbelin
2018-06-04Merge PR #7216: Replace uses of Termops.dependent by more specific functions.Matthieu Sozeau
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-04-10Replace uses of Termops.dependent by more specific functions.Pierre-Marie Pédrot
2018-03-31[econstr] Forbid calling `to_constr` in open terms.Emilio Jesus Gallego Arias
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-22[api] Deprecate Term destructors, move to ConstrEmilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.Maxime Dénès
2017-11-05Refining PR#924 (insensitivity of projection heuristics to alphabet).Hugo Herbelin
2017-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:42:37 +0000