aboutsummaryrefslogtreecommitdiff
path: root/kernel/safe_typing.ml
AgeCommit message (Expand)Author
2019-09-25Move the Lib section data into the kernel.Pierre-Marie Pédrot
2019-09-25Stub code for handling sections in kernel.Pierre-Marie Pédrot
2019-08-16Set/Unset commands for typing flagsSimonBoulier
2019-07-08Similar purity invariants in the kernel.Pierre-Marie Pédrot
2019-07-04Merge PR #10461: Simplify Declare.declare_variableEmilio Jesus Gallego Arias
2019-07-04Merge PR #10359: Remove dependency of native_compile on global env for symbolsMaxime Dénès
2019-07-03Safe_typing.push_named_assum: don't take universesGaëtan Gilbert
2019-06-27Kernel transparent definition entries have no body universes.Gaëtan Gilbert
2019-06-26Perform the opaque section variable inference outside of the kernel.Pierre-Marie Pédrot
2019-06-24Remove the unused opaque_entry_inline_code field from opaque entries.Pierre-Marie Pédrot
2019-06-24Enforce that opaque entries carry their type.Pierre-Marie Pédrot
2019-06-24Dedicated type for opaque entries in the kernel.Pierre-Marie Pédrot
2019-06-24Enforce that transparent entries are forced beforehand.Pierre-Marie Pédrot
2019-06-24Take advantage of the change of entry representation to split opacity status.Pierre-Marie Pédrot
2019-06-17Merge PR #10362: Kernel-side delaying of polymorphic opaque constantsGaëtan Gilbert
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17Clean up the code adding monomorphic global constraints in Safe_typing.Pierre-Marie Pédrot
2019-06-17Merge universe quantification and delayed constraints in opaque proofs.Pierre-Marie Pédrot
2019-06-17Allow to delay polymorphic opaque constants.Pierre-Marie Pédrot
2019-06-12Remove dependency of native_compile on global env for symbolsGaëtan Gilbert
2019-06-11Remove the side-effect role from the kernel.Pierre-Marie Pédrot
2019-06-11Move type definition Nativecode.symbols to NativevaluesGaëtan Gilbert
2019-06-06Merge the two sources of monomorphic constraints for side-effects.Pierre-Marie Pédrot
2019-06-04Do not substitute opaque constants when discharging.Pierre-Marie Pédrot
2019-05-27Merge PR #10249: More precise type for export and inlining of private constantsMaxime Dénès
2019-05-26More precise type for Safe_typing export and inlining of private constants.Pierre-Marie Pédrot
2019-05-25Centralize the hashconsing of constant declarations.Pierre-Marie Pédrot
2019-05-24Remove a last use of opacity-piercing function in Safe_typing.Pierre-Marie Pédrot
2019-05-20Ensure statically that declarations built by Term_typing are direct.Pierre-Marie Pédrot
2019-05-19Parameterize the constant_body type by opaque subproofs.Pierre-Marie Pédrot
2019-05-19Merge the definition of constants and private constants in the API.Pierre-Marie Pédrot
2019-05-15Simplify the private constant API.Pierre-Marie Pédrot
2019-05-14Abstract away the implementation of side-effects in Safe_typing.Pierre-Marie Pédrot
2019-03-18Remove Term_typing.translate_mind indirectionGaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-02-26Fix #9526: Registering inductives for primitive integers doesn't check enoughMaxime Dénès
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-08Remove global output_native_objects flag.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
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-23Merge PR #8995: Don't redeclare constraints of fields in IncludeMaxime Dénès
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-16Don't redeclare constraints of fields in IncludeGaëtan Gilbert
2018-11-15Make set_typing_flags "smart"Gaëtan Gilbert
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-11-06[checker] Refactor by sharing code with the kernelMaxime Dénès
2018-11-05Pass native and VM flags to the kernel through environmentMaxime Dénès
2018-10-31Use standard combinator for Global.set_strategyMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:58:13 +0000