aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarsolve.mli
AgeCommit message (Expand)Author
2020-11-21Short documentation of solve_simple_eqn.Hugo Herbelin
2020-11-16Fixing the "IllTypedInstance" anomaly part of #5512.Hugo Herbelin
2020-09-03Comment AllowedEvars APIMaxime Dénès
2020-09-02Abstract type for allowed evarsMaxime Dénès
2020-09-02Replace `frozen` by `allowed` evars in evarconv, and delay themMaxime Dénès
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
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-02-08evarsolve transp_state and comments fixesMatthieu Sozeau
2019-02-08Document the unify_flags more throroughly in evarsolve.Matthieu 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-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Dedicated datatype for aliases in Evarsolve.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers in RetypingPierre-Marie Pédrot
2017-02-14Unification API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarsolve API using EConstr.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-10-22Renamings to avoid confusion deprecating old namesMatthieu Sozeau
2016-07-04congruence: Restrict refreshing to SetMatthieu Sozeau
2016-07-04congruence/univs: properly refresh (fix #4609)Matthieu Sozeau
2016-01-20Update copyright headers.Maxime Dénès
2015-11-11Fix bug #4293: ensure let-ins do not contain algebraic universes inMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-10-02Work around issues with FO unification trying to unify terms ofMatthieu Sozeau
2014-09-19Move the specific map_constr_with_binders_left_to_rightMatthieu Sozeau
2014-09-18Fix constrMatching as well as change/e_contextually to allowMatthieu Sozeau
2014-08-26Make evarconv and unification able to handle eta for records in presenceMatthieu Sozeau
2014-08-25Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleMatthieu Sozeau
2014-07-30Avoid introducing additional universes when doing pruning in evarsolve.Matthieu Sozeau
2014-06-26Change interface of refresh universes to get a pbty argument instead ofMatthieu Sozeau
2014-06-21- Add an option to refresh only algebraic universes, for e_type_of. The goalMatthieu Sozeau
2014-06-20Cleanup treatment of template universe polymorphism (thanks to E. TassiMatthieu Sozeau
2014-05-06Find a more efficient fix for dealing with template universes:Matthieu Sozeau
2014-05-06Try a new way of handling template universe levelsMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-01Propagating conversion_problem towards (postponed) evar/evar problems.Hugo Herbelin
2013-10-22Removing useless array-to-list and converse casts used inppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:51:44 +0000