aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.mli
AgeCommit message (Expand)Author
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
2017-02-14Moving printing code from Evd to Termops.Pierre-Marie Pédrot
2017-02-14Chasing a few unsafe constr coercions.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2017-02-14Ltac now uses evar-based constrs.Pierre-Marie Pédrot
2016-12-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-12-02Document changesMatthieu Sozeau
2016-11-30Fix UGraph.check_eq!Matthieu Sozeau
2016-10-30Reordering Termops w.r.t. Evd and Namegen in engine folder.Pierre-Marie Pédrot
2016-09-01Short documentation, filling TODO's in evd.mli.Hugo Herbelin
2016-08-10Remove unused optional "predicative" argument.Guillaume Melquiond
2016-06-29Univs: add source locations of levelsMatthieu Sozeau
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-02-19Allowing to attach location to universes in UState.Pierre-Marie Pédrot
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-11mergeMatej Kosik
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:09:36 +0000