aboutsummaryrefslogtreecommitdiff
path: root/kernel/environ.mli
AgeCommit message (Expand)Author
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
2016-06-18Reuse the typing_flags datatype for inductives.Pierre-Marie Pédrot
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-18Adding a local type-in-type flag in kernel declarations.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Adds support for the virtual machine to perform reduction of universe polymor...Gregory Malecha
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-10-02Forcing i > Set for global universes (incomplete)Matthieu Sozeau
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-03-25Fix vm compiler to refuse to compile code making use of inductives withMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-11-12Cleaner interfaces for linking locations of native compiler.Maxime Dénès
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-09-24Make the retroknowledge marshalable.Arnaud Spiwack
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-06-13Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).Hugo Herbelin
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06- Rename eq to equal in Univ, document new modules, set interfaces.Matthieu Sozeau
2014-05-06Fix interface for template polymorphism, cleaning up code in all typing algor...Matthieu Sozeau
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 06:23:49 +0000