aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarconv.mli
AgeCommit message (Expand)Author
2021-03-26[recordops] complete API rewrite; the module is now called [structures]Enrico Tassi
2020-11-26extracting API for comparing universes of constants/inductives/constructorsbeta
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-03-18Update headers in the whole code base.Théo Zimmermann
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-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-05-07Do not use the constant stack in whd_betaiota_deltazeta_for_iota_state.Pierre-Marie Pédrot
2019-02-08evarconf transp state and comments fixesMatthieu Sozeau
2019-02-08Add back the deprecated conv/cumul functions.Matthieu Sozeau
2019-02-08Change interfaces of evarconv as suggested by Enrico.Matthieu Sozeau
2019-02-08[occur_rigidly] Try improving occur-check approximationMatthieu 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-08Abstraction namingMatthieu Sozeau
2019-02-08evarconv/evarsolve: HO matching algorithm with occurrence selectionMatthieu Sozeau
2019-02-08[evarconv] New flag handling for unifierMatthieu Sozeau
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-10-14Parameterizing default inhabitant for impossible cases with an environment.Hugo Herbelin
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-05-11set_solve_evars doesn't use an evar_map refGaëtan Gilbert
2018-05-11Deprecate Evarconv.e_conv,e_cumulGaëtan Gilbert
2018-05-11Deprecate most evarutil evdref functionsGaëtan Gilbert
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-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-05-27[coqlib] Move `Coqlib` to `library/`.Emilio Jesus Gallego Arias
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Evarconv API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2016-10-22Renamings to avoid confusion deprecating old namesMatthieu Sozeau
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-12-15Documenting check_record + changing a possibly undefined int into int option.Hugo Herbelin
2014-12-12Two fixes in unification (bugs #3782 and #3709)Matthieu Sozeau
2014-12-09Setup hook to change the unification algorithm used by evarconv,Matthieu Sozeau
2014-09-26Fix canonical structure resolution which was launched on the results ofMatthieu Sozeau
2014-06-11- Fix bug #3368, due to wrong use of the Cst_stack for projections.Matthieu Sozeau
2014-05-26Cst_stack before stack (abstraction leak in whd_gen)Pierre Boutillier
2014-05-06- Add back some compatibility functions to avoid rewriting plugins.Matthieu Sozeau
2014-05-06- Fixes for canonical structure resolution (check that the initial term indee...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-16consider_remaining_unif_problems respects Conv_oraclePierre Boutillier
2014-03-10Evarconv unification respects Conv_oraclePierre Boutillier
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:03:17 +0000