aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.mli
AgeCommit message (Expand)Author
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-17Split off Universes functions about substitutions and constraintsGaëtan Gilbert
2018-05-17Split off Universes functions dealing with names.Gaëtan Gilbert
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
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-08Merge PR #6893: Cleanup UState API usageMaxime Dénès
2018-03-06Rename some universe minimizing "normalize" functions to "minimize"Gaëtan Gilbert
2018-03-06Deprecate UState aliases in Evd.Gaëtan Gilbert
2018-03-05Add empty description for @raise statements to satisfy ocamldocmrmr1993
2018-03-05Replace invalid tag @raises in ocamldoc comments with @raisemrmr1993
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-12Merge PR #6275: [summary] Allow typed projections from global state.Maxime Dénès
2017-12-09[api] Remove yet another type alias.Emilio Jesus Gallego Arias
2017-12-09[summary] Adapt STM to the new Summary API.Emilio Jesus Gallego Arias
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-24Use type Universes.universe_binders.Gaëtan Gilbert
2017-11-22[api] A few more minor deprecation notices.Emilio Jesus Gallego Arias
2017-11-13[api] Insert miscellaneous API deprecation back to core.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-10-09Merge PR #1109: Handle some misc todosMaxime Dénès
2017-09-29Remove TODO comment (Evar.t is opaque)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-19proof_global: cleanup and comment close_proofMatthieu Sozeau
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-05Univs: fix bug #5365, generation of u+k <= v constraintsMatthieu Sozeau
2017-06-01Bump year in headers.Maxime Dénès
2017-05-30Support for using type information to infer more precise evar sources.Hugo Herbelin
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-07Merge branch 'master' into econstrPierre-Marie Pédrot
2017-03-23Ensuring static invariants about handling of pending evars in Pretyping.Pierre-Marie Pédrot
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Making Evd independent from Namegen.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:30:07 +0000