aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.ml
AgeCommit message (Expand)Author
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
2017-11-25Forbid repeated names in universe binders.Gaëtan Gilbert
2017-11-24Use Entries.constant_universes_entry more.Gaëtan Gilbert
2017-11-24Stop exposing UState.universe_context and its Evd wrapper.Gaëtan Gilbert
2017-11-24Separate checking univ_decls and obtaining universe binder names.Gaëtan Gilbert
2017-11-24Use Maps and ids for universe bindersGaëtan Gilbert
2017-11-22[api] Deprecate Term destructors, move to ConstrEmilio Jesus Gallego Arias
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
2017-11-01Fix FIXME: use OCaml 4.02 generative functors when available.Gaëtan Gilbert
2017-09-27Moving setting of "cleared" evar flag directly in Evd.restrict.Hugo Herbelin
2017-09-19Don't lose names in UState.universe_context.Gaëtan Gilbert
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-07-04Merge branch 'v8.6'Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-15Merge PR#713: Bump year in headers.Maxime Dénès
2017-06-14Fixing restrict regarding evar_store.Hugo Herbelin
2017-06-05Univs: fix bug #5365, generation of u+k <= v constraintsMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:27:15 +0000