aboutsummaryrefslogtreecommitdiff
path: root/kernel/environ.mli
AgeCommit message (Expand)Author
2019-05-24Move body_of_constant_body to Global and specialize its uses.Pierre-Marie Pédrot
2019-05-21Merge PR #10174: Further cleanup of the side-effect machineryGaëtan Gilbert
2019-05-19Parameterize the constant_body type by opaque subproofs.Pierre-Marie Pédrot
2019-05-11Generalize map_named_val to handle whole declarations.Pierre-Marie Pédrot
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-02-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
2019-02-05Merge PR #9438: Cleanup universe length for inductives in vconvPierre-Marie Pédrot
2019-02-04Primitive integersMaxime Dénès
2019-01-30Cleanup universe length for inductives in vconvGaëtan Gilbert
2019-01-21Refactor typechecking of inductive typesGaëtan Gilbert
2018-11-27Merge PR #8850: Private universes for opaque polymorphic constants.Matthieu Sozeau
2018-11-26Put -indices-matter in typing_flagsGaëtan Gilbert
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-05Merge PR #8866: Check universe instances in TypingPierre-Marie Pédrot
2018-10-31Seeing Global purely as a wrapper on top of kernel functions.Hugo Herbelin
2018-10-30Remove Environ.set_universes / Typing.enrich_envGaëtan Gilbert
2018-10-24Comment Environ.set_universesGaëtan Gilbert
2018-10-16Simplify vars_of_global usageGaëtan Gilbert
2018-10-16Deprecate Global.universes_of_global (replaced by environ version)Gaëtan Gilbert
2018-10-11A state-free version of is_polymorphic.Hugo Herbelin
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-09-14Retroknowledge: use GlobRef.t instead of Constr.t as entryVincent Laporte
2018-07-24Projections use index representationGaëtan Gilbert
2018-06-29Merge PR #7080: Swapping Context and Constr and defining declarations on cons...Maxime Dénès
2018-06-28Deprecate Environ.retroknowledge function in favor of the projectionGaëtan Gilbert
2018-06-28Make Environ.globals abstract.Gaëtan Gilbert
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
2018-05-28Unify pre_env and envMaxime Dénès
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
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-01-20Remove dead code in Environ.Pierre-Marie Pédrot
2017-12-09[api] Remove yet another type alias.Emilio Jesus Gallego Arias
2017-11-26[api] Remove aliases of `Evar.t`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-09-28Efficient computation of the names contained in an environment.Pierre-Marie Pédrot
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-11Safe API for accessing universe constraints of global references.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-02-14Making judgment type generic over the type of inner constrs.Pierre-Marie Pédrot
2016-10-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-12Remove dead code in Environ.Pierre-Marie Pédrot
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-09Removing the now useless field env_named_val from named_context_val.Pierre-Marie Pédrot
2016-09-09Packing the named_context_val in a proper record and marking it private.Pierre-Marie Pédrot
2016-08-25CLEANUP: Type alias "Context.section_context" was removedMatej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:25:34 +0000