aboutsummaryrefslogtreecommitdiff
path: root/kernel/environ.ml
AgeCommit message (Expand)Author
2020-11-15Merge PR #13356: Make the universe of primitive arrays irrelevantPierre-Marie Pédrot
2020-11-13Make the universe of primitive arrays irrelevantGaëtan Gilbert
2020-11-12Merge the Linked and LinkedInteractive constructors.Pierre-Marie Pédrot
2020-11-09Remove the native symbol registering from the safe environment.Pierre-Marie Pédrot
2020-10-21Introduce the missing dual name quotient modules in Environ.Pierre-Marie Pédrot
2020-10-21Introduce a dummy name quotient API.Pierre-Marie Pédrot
2020-10-09No bidirectionality when expected type for lambda is an evar.Gaëtan Gilbert
2020-09-28Put type-in-type flag in ugraph.Gaëtan Gilbert
2020-08-06Store the default instance in named_context_val.Pierre-Marie Pédrot
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-01UIP in SPropGaëtan Gilbert
2020-05-13Make explicit that UGraph lower bounds are only of two kinds.Pierre-Marie Pédrot
2020-04-30Merge PR #12107: Remove mod_constraints field of module bodyPierre-Marie Pédrot
2020-04-20Remove mod_constraints field of module bodyGaëtan Gilbert
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-08Ensure that template parameters are shared in the same inductive block.Pierre-Marie Pédrot
2020-02-12Merge PR #11569: Remove unused Environ.push_constraints_to_envPierre-Marie Pédrot
2020-02-11Remove unused Environ.push_constraints_to_envGaëtan Gilbert
2020-02-09Remove the Template Check option.Pierre-Marie Pédrot
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-10-24Raise an anomaly when looking up unknown constant/inductiveGaëtan Gilbert
2019-10-07(Partially) Revert "Make Environ.globals abstract."Emilio Jesus Gallego Arias
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-16Fix typing_flags in the checkerSimonBoulier
2019-08-16Set/Unset commands for typing flagsSimonBoulier
2019-07-04Merge PR #10359: Remove dependency of native_compile on global env for symbolsMaxime Dénès
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-12Remove dependency of native_compile on global env for symbolsGaëtan Gilbert
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 relevance marks on binders.Gaëtan Gilbert
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-15Make set_typing_flags "smart"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-30Simplify universe handling in environ constant_type functionsGaëtan Gilbert
2018-10-16Simplify vars_of_global usageGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:20:06 +0000