aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.ml
AgeCommit message (Expand)Author
2019-05-21Merge PR #10144: Fix #9919: conversion functions are non-linearHugo Herbelin
2019-05-13Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.Hugo Herbelin
2019-05-11Generalize map_named_val to handle whole declarations.Pierre-Marie Pédrot
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-03-14Make Sorts.t privateGaëtan Gilbert
2019-03-12Merge PR #7819: Ho matching occ selEnrico Tassi
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-08Abstraction namingMatthieu Sozeau
2019-02-08Evd/evarsolve: add an abstraction field to evars for unificationMatthieu Sozeau
2019-01-21[EConstr] Expose API to normalize and check if evars are remainingMaxime Dénès
2018-12-17Add Map.find_optGaëtan Gilbert
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-30Switch to using the obligation_evar flag instead of the evar sourceMatthieu 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 fresh_foo_instance functions and pretyping of univ instanceGaëtan Gilbert
2018-09-12Merge PR #7109: Term combinators respecting the canonical structure of branch...Maxime Dénès
2018-09-03Adding combinators preserving expanded form of branches and pred. of "match".Hugo Herbelin
2018-07-25Fix #7900 previous commit fixes a bug when using side effects in obligations.Matthieu Sozeau
2018-07-03Remove unused function Evd.whd_sort_variableGaëtan Gilbert
2018-07-03Remove unused env argument to fresh_sort_in_familyGaëtan Gilbert
2018-06-27Merge PR #7863: Remove Sorts.contentsPierre-Marie Pédrot
2018-06-26Merge PR #7826: evd: restrict_evar with candidates, can raise NoCandidatesLeftHugo Herbelin
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-23Merge PR #7827: [engine] safe [add_unification_pb] interfacePierre-Marie Pédrot
2018-06-18Fix #7421: constr_eq ignores universe constraints.Gaëtan Gilbert
2018-06-15evd: restrict_evar with candidates, can raise NoCandidatesLeftMatthieu Sozeau
2018-06-15evd/evarutil: safe [add_unification_pb] interface, taking EConstr'sMatthieu Sozeau
2018-05-30[api] Remove deprecated objects in engine / interp / libraryEmilio Jesus Gallego Arias
2018-05-23Collecting Map.smart_* functions into a module Map.Smart.Hugo Herbelin
2018-05-17Split off Universes functions about substitutions and constraintsGaëtan Gilbert
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-05-08Don't use ref universe_opt_substGaëtan Gilbert
2018-04-29Implement to_constr with nf_evars_and_universes_opt_substGaëtan Gilbert
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-03-09Statically enforce that ULub is only between levels.Gaëtan Gilbert
2018-03-08Proof engine: support for nesting tactic-in-term within other tactics.Hugo Herbelin
2018-03-08Proof engine: adding a function to save future goals including principal one.Hugo Herbelin
2018-03-08Proof engine: consider the pair principal and future goals as an entity.Hugo Herbelin
2018-03-06Rename some universe minimizing "normalize" functions to "minimize"Gaëtan Gilbert
2018-03-06Deprecate UState aliases in Evd.Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2017-12-30Moving some universe substitution code out of the kernel.Pierre-Marie Pédrot
2017-12-09[summary] Adapt STM to the new Summary API.Emilio Jesus Gallego Arias
2017-12-05Rename update to set, fixes #6196Paul Steckler
2017-11-28Merge PR #1033: Universe binder improvementsMaxime Dénès
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:40:07 +0000