aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarsolve.ml
AgeCommit message (Expand)Author
2020-11-16Merge PR #12873: Unification: A type-checking fix in imitation + an error loc...coqbot-app[bot]
2020-11-16Checking type in unification imitation: avoid raising a non-located error.Hugo Herbelin
2020-11-16Fixing a (known) "bugged" part of imitation in unification.Hugo Herbelin
2020-11-15Fixes #12348: long-standing de Bruijn indices bug in imitation (solve_simple_...Hugo Herbelin
2020-11-15Locating the Ill-typed evar instance error.Hugo Herbelin
2020-09-28More precise information when unification fails because of incompatible candi...Hugo Herbelin
2020-09-02More efficient data structure for allowed evarsMaxime 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-08-06Use the evarinfo-stored identity substitution where applicable.Pierre-Marie Pédrot
2020-07-08Remove Evarutil.new_evar_instance from the API.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:59:35 +0000